diff --git a/idris2api.ipkg b/idris2api.ipkg index cffd0aeab..5405b2285 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -49,6 +49,7 @@ modules = Core.Binary.Prims, Core.Case.CaseBuilder, Core.Case.CaseTree, + Core.Case.CaseTree.Pretty, Core.Case.Util, Core.CompileExpr, Core.CompileExpr.Pretty, diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 24fd76c61..3fca558d3 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -287,12 +287,14 @@ dconFlag n = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (InternalError ("Can't find " ++ show n)) - pure (ciFlags (flags def)) + pure (ciFlags (definition def) (flags def)) where - ciFlags : List DefFlag -> ConInfo - ciFlags [] = DATACON - ciFlags (ConType ci :: xs) = ci - ciFlags (x :: xs) = ciFlags xs + ciFlags : Def -> List DefFlag -> ConInfo + ciFlags def [] = case def of + TCon{} => TYCON + _ => DATACON + ciFlags def (ConType ci :: xs) = ci + ciFlags def (x :: xs) = ciFlags def xs mutual toCExpTm : {vars : _} -> diff --git a/src/Core/Case/CaseTree.idr b/src/Core/Case/CaseTree.idr index cc83cea3d..c11b001f5 100644 --- a/src/Core/Case/CaseTree.idr +++ b/src/Core/Case/CaseTree.idr @@ -143,32 +143,6 @@ covering {vars : _} -> Show (CaseAlt vars) where show = showCA "" -mutual - export - {vars : _} -> Pretty IdrisSyntax (CaseTree vars) where - pretty (Case {name} idx prf ty alts) - = case_ <++> pretty0 name <++> keyword ":" <++> byShow ty <++> of_ - <+> nest 2 (hardline - <+> vsep (assert_total (map pretty alts))) - pretty (STerm i tm) = byShow tm - pretty (Unmatched msg) = "Error:" <++> pretty0 msg - pretty Impossible = "Impossible" - - export - {vars : _} -> Pretty IdrisSyntax (CaseAlt vars) where - pretty (ConCase n tag args sc) - = hsep (map pretty0 (n :: args)) <++> fatArrow - <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc)) - pretty (DelayCase _ arg sc) = - keyword "Delay" <++> pretty0 arg <++> fatArrow - <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc)) - pretty (ConstCase c sc) = - pretty c <++> fatArrow - <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc)) - pretty (DefaultCase sc) = - keyword "_" <++> fatArrow - <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc)) - mutual export eqTree : CaseTree vs -> CaseTree vs' -> Bool diff --git a/src/Core/Case/CaseTree/Pretty.idr b/src/Core/Case/CaseTree/Pretty.idr new file mode 100644 index 000000000..493ed50d3 --- /dev/null +++ b/src/Core/Case/CaseTree/Pretty.idr @@ -0,0 +1,104 @@ +module Core.Case.CaseTree.Pretty + +import Core.Context +import Core.Env +import Core.TT +import Core.Case.CaseTree +import Idris.Syntax +import Idris.Pretty +import Idris.Resugar + +import Data.String +import Libraries.Data.String.Extra +import Libraries.Text.PrettyPrint.Prettyprinter + +namespace Raw + + export + prettyTree : {vars : _} -> CaseTree vars -> Doc IdrisSyntax + prettyAlt : {vars : _} -> CaseAlt vars -> Doc IdrisSyntax + + prettyTree (Case {name} idx prf ty alts) + = let ann = case ty of + Erased _ _ => "" + _ => space <+> keyword ":" <++> byShow ty + in case_ <++> annotate Bound (pretty0 name) <+> ann <++> of_ + <+> nest 2 (hardline + <+> vsep (assert_total (map prettyAlt alts))) + prettyTree (STerm i tm) = byShow tm + prettyTree (Unmatched msg) = "Error:" <++> pretty0 msg + prettyTree Impossible = "Impossible" + + prettyAlt (ConCase n tag args sc) + = hsep (annotate (DCon (Just n)) (pretty0 n) :: map pretty0 args) + <++> fatArrow + <+> let sc = prettyTree sc in + Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) + prettyAlt (DelayCase _ arg sc) = + keyword "Delay" <++> pretty0 arg + <++> fatArrow + <+> let sc = prettyTree sc in + Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) + prettyAlt (ConstCase c sc) = + pretty c + <++> fatArrow + <+> let sc = prettyTree sc in + Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) + prettyAlt (DefaultCase sc) = + keyword "_" + <++> fatArrow + <+> let sc = prettyTree sc in + Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) + +namespace Resugared + + prettyName : {auto c : Ref Ctxt Defs} -> + Name -> Core (Doc IdrisSyntax) + prettyName nm + = pure $ ifThenElse (fullNamespace !(getPPrint)) + (pretty0 nm) + (cast $ prettyOp True $ dropNS nm) + + export + prettyTree : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Env Term vars -> CaseTree vars -> Core (Doc IdrisSyntax) + prettyAlt : {vars : _} -> + {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Env Term vars -> CaseAlt vars -> Core (Doc IdrisSyntax) + + prettyTree env (Case {name} idx prf ty alts) = do + ann <- case ty of + Erased _ _ => pure "" + _ => do ty <- resugar env ty + pure (space <+> keyword ":" <++> pretty ty) + alts <- assert_total (traverse (prettyAlt env) alts) + pure $ case_ <++> pretty0 name <+> ann <++> of_ + <+> nest 2 (hardline <+> vsep alts) + prettyTree env (STerm i tm) = pretty <$> resugar env tm + prettyTree env (Unmatched msg) = pure ("Error:" <++> pretty0 msg) + prettyTree env Impossible = pure "Impossible" + + prettyAlt env (ConCase n tag args sc) = do + con <- prettyName n + sc <- prettyTree (mkEnvOnto emptyFC args env) sc + pure $ hsep (annotate (DCon (Just n)) con :: map pretty0 args) + <++> fatArrow + <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) + prettyAlt env (DelayCase _ arg sc) = do + sc <- prettyTree (mkEnvOnto emptyFC [_,_] env) sc + pure $ keyword "Delay" <++> pretty0 arg + <++> fatArrow + <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) + prettyAlt env (ConstCase c sc) = do + sc <- prettyTree env sc + pure $ pretty c + <++> fatArrow + <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) + prettyAlt env (DefaultCase sc) = do + sc <- prettyTree env sc + pure $ keyword "_" + <++> fatArrow + <+> Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc)) diff --git a/src/Core/CompileExpr/Pretty.idr b/src/Core/CompileExpr/Pretty.idr index 219c2f9aa..745046114 100644 --- a/src/Core/CompileExpr/Pretty.idr +++ b/src/Core/CompileExpr/Pretty.idr @@ -37,21 +37,22 @@ import Libraries.Data.String.Extra %hide Pretty.Syntax %hide List1.forget -prettyFlag : ConInfo -> Doc ann -prettyFlag DATACON = "" -prettyFlag f = pretty0 (show f) +prettyFlag : ConInfo -> Maybe (Doc ann) +prettyFlag DATACON = Nothing +prettyFlag f = Just (byShow f) prettyCon : Name -> ConInfo -> Maybe Int -> Doc IdrisSyntax -prettyCon x ci tag - = hsep [ annotate (DCon (Just x)) (pretty0 x) - , braces ("tag =" <++> byShow tag) - , prettyFlag ci - ] +prettyCon x ci mtag + = hsep $ catMaybes + [ Just (annotate ((if ci == TYCON then TCon else DCon) (Just x)) (pretty0 x)) + , (braces . ("tag =" <++>) . byShow) <$> mtag + , prettyFlag ci + ] mutual Pretty IdrisSyntax NamedCExp where - prettyPrec d (NmLocal _ x) = "!" <+> pretty0 x - prettyPrec d (NmRef _ x) = pretty0 x + prettyPrec d (NmLocal _ x) = annotate Bound $ pretty0 x + prettyPrec d (NmRef _ x) = annotate (Fun x) $ pretty0 x prettyPrec d (NmLam _ x y) = parenthesise (d > Open) $ keyword "\\" <+> pretty0 x <+> fatArrow <++> pretty y prettyPrec d (NmLet _ x y z) @@ -82,7 +83,8 @@ mutual prettyPrec d (NmErased _) = "___" prettyPrec d (NmCrash _ x) = parenthesise (d > Open) $ - sep ["crash", pretty0 x] + sep [annotate Keyword "crash", byShow x] + Pretty IdrisSyntax NamedConAlt where pretty (MkNConAlt x ci tag args exp) = sep (prettyCon x ci tag :: map pretty0 args ++ [fatArrow <+> softline <+> align (pretty exp) ]) diff --git a/src/Core/Context/Pretty.idr b/src/Core/Context/Pretty.idr index 5568c7ed1..81baefbaf 100644 --- a/src/Core/Context/Pretty.idr +++ b/src/Core/Context/Pretty.idr @@ -1,15 +1,22 @@ module Core.Context.Pretty +import Core.Context +import Core.Env + import Data.String import Idris.Doc.Annotations +import Idris.Syntax import Idris.Pretty import Core.Case.CaseTree +import Core.Case.CaseTree.Pretty import Core.Context.Context import Libraries.Data.String.Extra +%hide Env.(::) +%hide Env.Nil %hide String.(::) %hide String.Nil %hide Doc.Nil @@ -29,49 +36,103 @@ import Libraries.Data.String.Extra %default covering -export -Pretty IdrisDocAnn Def where - pretty None = "undefined" - pretty (PMDef _ args ct _ pats) - = vcat [ "Arguments" <++> cast (prettyList args) - , header "Compile time tree" <++> prettyBy Syntax ct - ] - pretty (DCon tag arity nt) - = vcat $ header "Data constructor" :: map (indent 2) - ([ "tag:" <++> byShow tag - , "arity:" <++> byShow arity - ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt) - pretty (TCon tag arity ps ds u ms cons det) - = let enum = hsep . punctuate "," in - vcat $ header "Type constructor" :: map (indent 2) - ([ "tag:" <++> byShow tag - , "arity:" <++> byShow arity - , "parameter positions:" <++> byShow ps - , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons) - ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms)) - ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det)) - pretty (ExternDef arity) - = vcat $ header "External definition" :: map (indent 2) - [ "arity:" <++> byShow arity ] - pretty (ForeignDef arity calls) - = vcat $ header "Foreign definition" :: map (indent 2) - [ "arity:" <++> byShow arity - , "bindings:" <++> byShow calls ] - pretty (Builtin {arity} _) - = vcat $ header "Builtin" :: map (indent 2) - [ "arity:" <++> byShow arity ] - pretty (Hole numlocs hf) - = vcat $ header "Hole" :: map (indent 2) - ("Implicitly bound name" <$ guard (implbind hf)) - pretty (BySearch rig depth def) - = vcat $ header "Search" :: map (indent 2) - [ "depth:" <++> byShow depth - , "in:" <++> pretty0 def ] - pretty (Guess tm _ cs) - = vcat $ header "Guess" :: map (indent 2) - [ "solution:" <++> byShow tm - , "when:" <++> byShow cs ] - pretty (UniverseLevel i) - = "Universe level #" <+> byShow i - pretty ImpBind = "Bound name" - pretty Delayed = "Delayed" +namespace Raw + export + prettyDef : Def -> Doc IdrisDocAnn + prettyDef None = "undefined" + prettyDef (PMDef _ args ct _ pats) = + let ct = prettyTree ct in + vcat + [ "Arguments" <++> cast (prettyList args) + , header "Compile time tree" <++> reAnnotate Syntax ct + ] + prettyDef (DCon tag arity nt) = + vcat $ header "Data constructor" :: map (indent 2) + ([ "tag:" <++> byShow tag + , "arity:" <++> byShow arity + ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt) + prettyDef (TCon tag arity ps ds u ms cons det) = + let enum = hsep . punctuate "," in + vcat $ header "Type constructor" :: map (indent 2) + ([ "tag:" <++> byShow tag + , "arity:" <++> byShow arity + , "parameter positions:" <++> byShow ps + , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons) + ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms)) + ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det)) + prettyDef (ExternDef arity) = + vcat $ header "External definition" :: map (indent 2) + [ "arity:" <++> byShow arity ] + prettyDef (ForeignDef arity calls) = + vcat $ header "Foreign definition" :: map (indent 2) + [ "arity:" <++> byShow arity + , "bindings:" <++> byShow calls ] + prettyDef (Builtin {arity} _) = + vcat $ header "Builtin" :: map (indent 2) + [ "arity:" <++> byShow arity ] + prettyDef (Hole numlocs hf) = + vcat $ header "Hole" :: map (indent 2) + ("Implicitly bound name" <$ guard (implbind hf)) + prettyDef (BySearch rig depth def) = + vcat $ header "Search" :: map (indent 2) + [ "depth:" <++> byShow depth + , "in:" <++> pretty0 def ] + prettyDef (Guess tm _ cs) = + vcat $ header "Guess" :: map (indent 2) + [ "solution:" <++> byShow tm + , "when:" <++> byShow cs ] + prettyDef (UniverseLevel i) = "Universe level #" <+> byShow i + prettyDef ImpBind = "Bound name" + prettyDef Delayed = "Delayed" + +namespace Resugared + + export + prettyDef : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Def -> Core (Doc IdrisDocAnn) + prettyDef None = pure "undefined" + prettyDef (PMDef _ args ct _ pats) = do + ct <- prettyTree (mkEnv emptyFC _) ct + pure $ vcat + [ "Arguments" <++> cast (prettyList args) + , header "Compile time tree" <++> reAnnotate Syntax ct + ] + prettyDef (DCon tag arity nt) = pure $ + vcat $ header "Data constructor" :: map (indent 2) + ([ "tag:" <++> byShow tag + , "arity:" <++> byShow arity + ] ++ maybe [] (\ n => ["newtype by:" <++> byShow n]) nt) + prettyDef (TCon tag arity ps ds u ms cons det) = pure $ + let enum = hsep . punctuate "," in + vcat $ header "Type constructor" :: map (indent 2) + ([ "tag:" <++> byShow tag + , "arity:" <++> byShow arity + , "parameter positions:" <++> byShow ps + , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons) + ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms)) + ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det)) + prettyDef (ExternDef arity) = pure $ + vcat $ header "External definition" :: map (indent 2) + [ "arity:" <++> byShow arity ] + prettyDef (ForeignDef arity calls) = pure $ + vcat $ header "Foreign definition" :: map (indent 2) + [ "arity:" <++> byShow arity + , "bindings:" <++> byShow calls ] + prettyDef (Builtin {arity} _) = pure $ + vcat $ header "Builtin" :: map (indent 2) + [ "arity:" <++> byShow arity ] + prettyDef (Hole numlocs hf) = pure $ + vcat $ header "Hole" :: map (indent 2) + ("Implicitly bound name" <$ guard (implbind hf)) + prettyDef (BySearch rig depth def) = pure $ + vcat $ header "Search" :: map (indent 2) + [ "depth:" <++> byShow depth + , "in:" <++> pretty0 def ] + prettyDef (Guess tm _ cs) = pure $ + vcat $ header "Guess" :: map (indent 2) + [ "solution:" <++> byShow tm + , "when:" <++> byShow cs ] + prettyDef (UniverseLevel i) = pure $ "Universe level #" <+> byShow i + prettyDef ImpBind = pure "Bound name" + prettyDef Delayed = pure "Delayed" diff --git a/src/Core/Env.idr b/src/Core/Env.idr index 3ad02ab27..63909358f 100644 --- a/src/Core/Env.idr +++ b/src/Core/Env.idr @@ -17,6 +17,7 @@ export extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars) extend x = (::) {x} + export length : Env tm xs -> Nat length [] = 0 @@ -250,6 +251,13 @@ shrinkEnv (b :: env) (KeepCons p) b' <- assert_total (shrinkBinder b p) pure (b' :: env') +export +mkEnvOnto : FC -> (xs : List Name) -> Env Term ys -> Env Term (xs ++ ys) +mkEnvOnto fc [] vs = vs +mkEnvOnto fc (n :: ns) vs + = PVar fc top Explicit (Erased fc False) + :: mkEnvOnto fc ns vs + -- Make a dummy environment, if we genuinely don't care about the values -- and types of the contents. -- We use this when building and comparing case trees. diff --git a/src/Core/Name.idr b/src/Core/Name.idr index 1ca2acb51..f36fdcc42 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -287,11 +287,11 @@ mutual Pretty Void Name where pretty (NS ns n) = pretty ns <+> dot <+> prettyOp True n pretty (UN x) = pretty x - pretty (MN x y) = braces (pretty x <+> colon <+> pretty (show y)) - pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty (show d)) + pretty (MN x y) = braces (pretty x <+> colon <+> byShow y) + pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> byShow d) pretty (DN str _) = pretty str pretty (Nested (outer, idx) inner) - = pretty (show outer) <+> colon <+> pretty (show idx) <+> colon <+> pretty inner + = byShow outer <+> colon <+> byShow idx <+> colon <+> pretty inner pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer pretty (Resolved x) = pretty "$resolved" <+> pretty (show x) diff --git a/src/Core/Options.idr b/src/Core/Options.idr index e8809670c..d148e9b4c 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -184,6 +184,7 @@ public export record PPrinter where constructor MkPPOpts showImplicits : Bool + showMachineNames : Bool showFullEnv : Bool fullNamespace : Bool @@ -222,7 +223,7 @@ defaultDirs = MkDirs "." Nothing "build" "depends" Nothing "/usr/local" ["."] [] [] [] defaultPPrint : PPrinter -defaultPPrint = MkPPOpts False True False +defaultPPrint = MkPPOpts False False True False export defaultSession : Session diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 1ccab9210..ac5a9f673 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -429,45 +429,45 @@ Show (PrimFn arity) where export prettyOp : PrimFn arity -> Vect arity (Doc IdrisSyntax) -> Doc IdrisSyntax -prettyOp (Add ty) [v1,v2] = v1 <++> "+" <++> v2 -prettyOp (Sub ty) [v1,v2] = v1 <++> "-" <++> v2 -prettyOp (Mul ty) [v1,v2] = v1 <++> "*" <++> v2 -prettyOp (Div ty) [v1,v2] = v1 <++> "`div`" <++> v2 -prettyOp (Mod ty) [v1,v2] = v1 <++> "`mod`" <++> v2 -prettyOp (Neg ty) [v] = "-" <++> v -prettyOp (ShiftL ty) [v1,v2] = "shiftl" <++> v1 <++> v2 -prettyOp (ShiftR ty) [v1,v2] = "shiftr" <++> v1 <++> v2 -prettyOp (BAnd ty) [v1,v2] = v1 <++> "&&" <++> v2 -prettyOp (BOr ty) [v1,v2] = v1 <++> "||" <++> v2 -prettyOp (BXOr ty) [v1,v2] = v1 <++> "`xor`" <++> v2 -prettyOp (LT ty) [v1,v2] = v1 <++> "<" <++> v2 -prettyOp (LTE ty) [v1,v2] = v1 <++> "<=" <++> v2 -prettyOp (EQ ty) [v1,v2] = v1 <++> "==" <++> v2 -prettyOp (GTE ty) [v1,v2] = v1 <++> ">=" <++> v2 -prettyOp (GT ty) [v1,v2] = v1 <++> ">" <++> v2 -prettyOp StrLength [v] = "length" <++> v -prettyOp StrHead [v] = "head" <++> v -prettyOp StrTail [v] = "tail" <++> v -prettyOp StrIndex [v1,v2] = v1 <++> "[" <+> v2 <+> "]" -prettyOp StrCons [v1,v2] = v1 <++> "::" <++> v2 -prettyOp StrAppend [v1,v2] = v1 <++> "++" <++> v2 -prettyOp StrReverse [v] = "reverse" <++> v -prettyOp StrSubstr [v1,v2,v3] = v1 <++> "[" <+> v2 <+> "," <++> v3 <+> "]" -prettyOp DoubleExp [v] = "exp" <++> v -prettyOp DoubleLog [v] = "log" <++> v -prettyOp DoublePow [v1,v2] = v1 <++> "`pow`" <++> v2 -prettyOp DoubleSin [v] = "sin" <++> v -prettyOp DoubleCos [v] = "cos" <++> v -prettyOp DoubleTan [v] = "tan" <++> v -prettyOp DoubleASin [v] = "asin" <++> v -prettyOp DoubleACos [v] = "acos" <++> v -prettyOp DoubleATan [v] = "atan" <++> v -prettyOp DoubleSqrt [v] = "sqrt" <++> v -prettyOp DoubleFloor [v] = "floor" <++> v -prettyOp DoubleCeiling [v] = "ceiling" <++> v -prettyOp (Cast x y) [v] = "[" <+> pretty x <++> "->" <++> pretty y <+> "]" <++> v -prettyOp BelieveMe [v1,v2,v3] = "believe_me" <++> v1 <++> v2 <++> v3 -prettyOp Crash [v1,v2] = "crash" <++> v1 <++> v2 +prettyOp op@(Add ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "+" <++> v2 +prettyOp op@(Sub ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "-" <++> v2 +prettyOp op@(Mul ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "*" <++> v2 +prettyOp op@(Div ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`div`" <++> v2 +prettyOp op@(Mod ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`mod`" <++> v2 +prettyOp op@(Neg ty) [v] = annotate (Fun $ UN $ Basic $ show op) "-" <++> v +prettyOp op@(ShiftL ty) [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "shiftl" <++> v1 <++> v2 +prettyOp op@(ShiftR ty) [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "shiftr" <++> v1 <++> v2 +prettyOp op@(BAnd ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "&&" <++> v2 +prettyOp op@(BOr ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "||" <++> v2 +prettyOp op@(BXOr ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`xor`" <++> v2 +prettyOp op@(LT ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "<" <++> v2 +prettyOp op@(LTE ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "<=" <++> v2 +prettyOp op@(EQ ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "==" <++> v2 +prettyOp op@(GTE ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) ">=" <++> v2 +prettyOp op@(GT ty) [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) ">" <++> v2 +prettyOp op@StrLength [v] = annotate (Fun $ UN $ Basic $ show op) "length" <++> v +prettyOp op@StrHead [v] = annotate (Fun $ UN $ Basic $ show op) "head" <++> v +prettyOp op@StrTail [v] = annotate (Fun $ UN $ Basic $ show op) "tail" <++> v +prettyOp op@StrIndex [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "]" +prettyOp op@StrCons [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "::" <++> v2 +prettyOp op@StrAppend [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "++" <++> v2 +prettyOp op@StrReverse [v] = annotate (Fun $ UN $ Basic $ show op) "reverse" <++> v +prettyOp op@StrSubstr [v1,v2,v3] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "," <++> v3 <+> annotate (Fun $ UN $ Basic $ show op) "]" +prettyOp op@DoubleExp [v] = annotate (Fun $ UN $ Basic $ show op) "exp" <++> v +prettyOp op@DoubleLog [v] = annotate (Fun $ UN $ Basic $ show op) "log" <++> v +prettyOp op@DoublePow [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "`pow`" <++> v2 +prettyOp op@DoubleSin [v] = annotate (Fun $ UN $ Basic $ show op) "sin" <++> v +prettyOp op@DoubleCos [v] = annotate (Fun $ UN $ Basic $ show op) "cos" <++> v +prettyOp op@DoubleTan [v] = annotate (Fun $ UN $ Basic $ show op) "tan" <++> v +prettyOp op@DoubleASin [v] = annotate (Fun $ UN $ Basic $ show op) "asin" <++> v +prettyOp op@DoubleACos [v] = annotate (Fun $ UN $ Basic $ show op) "acos" <++> v +prettyOp op@DoubleATan [v] = annotate (Fun $ UN $ Basic $ show op) "atan" <++> v +prettyOp op@DoubleSqrt [v] = annotate (Fun $ UN $ Basic $ show op) "sqrt" <++> v +prettyOp op@DoubleFloor [v] = annotate (Fun $ UN $ Basic $ show op) "floor" <++> v +prettyOp op@DoubleCeiling [v] = annotate (Fun $ UN $ Basic $ show op) "ceiling" <++> v +prettyOp op@(Cast x y) [v] = annotate (Fun $ UN $ Basic $ show op) "[" <+> pretty x <++> annotate (Fun $ UN $ Basic $ show op) "->" <++> pretty y <+> annotate (Fun $ UN $ Basic $ show op) "]" <++> v +prettyOp op@BelieveMe [v1,v2,v3] = annotate (Fun $ UN $ Basic $ show op) "believe_me" <++> v1 <++> v2 <++> v3 +prettyOp op@Crash [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "crash" <++> v1 <++> v2 public export diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 739c6516f..fb9f84911 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -94,6 +94,10 @@ data CLOpt NoBanner | ||| Run Idris 2 in quiet mode Quiet | + ||| Show machine names when pretty printing + ShowMachineNames | + ||| Show namespaces when pretty printing + ShowNamespaces | ||| Run Idris 2 in verbose mode (cancels quiet if it's the default) Verbose | ||| Set the console width for REPL output @@ -267,7 +271,6 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--init"] [Optional "package file"] (\ f => [Package Init f]) (Just "Interactively initialise a new project"), - MkOpt ["--build"] [Optional "package file"] (\f => [Package Build f]) (Just "Build modules/executable for the given package"), @@ -313,6 +316,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] (Just "Quiet mode; display fewer messages"), MkOpt ["--console-width"] [AutoNat "console width"] (\l => [ConsoleWidth l]) (Just "Width for console output (0 for unbounded) (auto by default)"), + MkOpt ["--show-machine-names"] [] [ShowMachineNames] + (Just "Show machine names when pretty printing"), + MkOpt ["--show-namespaces"] [] [ShowNamespaces] + (Just "Show namespaces when pretty printing"), MkOpt ["--color", "--colour"] [] ([Color True]) (Just "Forces colored console output (enabled by default)"), MkOpt ["--no-color", "--no-colour"] [] ([Color False]) diff --git a/src/Idris/Doc/Display.idr b/src/Idris/Doc/Display.idr index d3b787d31..aaeafd73a 100644 --- a/src/Idris/Doc/Display.idr +++ b/src/Idris/Doc/Display.idr @@ -1,6 +1,7 @@ module Idris.Doc.Display import Core.Case.CaseTree +import Core.Case.CaseTree.Pretty import Core.Context import Core.Env diff --git a/src/Idris/IDEMode/Holes.idr b/src/Idris/IDEMode/Holes.idr index 6add037de..45634640d 100644 --- a/src/Idris/IDEMode/Holes.idr +++ b/src/Idris/IDEMode/Holes.idr @@ -27,24 +27,16 @@ impBracket : Bool -> String -> String impBracket False str = str impBracket True str = "{" ++ str ++ "}" -tidy : Name -> String -tidy (MN n _) = n -tidy n = show n - export covering Show Holes.Premise where show premise = " " ++ showCount premise.multiplicity ++ " " - ++ impBracket premise.isImplicit (tidy premise.name ++ " : " ++ show premise.type) + ++ impBracket premise.isImplicit (show premise.name ++ " : " ++ show premise.type) prettyImpBracket : Bool -> Doc ann -> Doc ann prettyImpBracket False = id prettyImpBracket True = braces -prettyName : Name -> Doc IdrisSyntax -prettyName (MN n _) = pretty0 n -prettyName n = pretty0 n - export prettyRigHole : RigCount -> Doc IdrisSyntax prettyRigHole = elimSemi (keyword (pretty0 '0') <+> space) @@ -55,7 +47,7 @@ export Pretty IdrisSyntax Holes.Premise where pretty premise = prettyRigHole premise.multiplicity - <+> prettyImpBracket premise.isImplicit (prettyName premise.name <++> colon <++> pretty premise.type) + <+> prettyImpBracket premise.isImplicit (pretty0 premise.name <++> colon <++> pretty premise.type) public export record Data where @@ -201,7 +193,7 @@ premiseIDE : Holes.Premise -> HolePremise premiseIDE premise = IDE.MkHolePremise { name = " " ++ showCount premise.multiplicity ++ " " ++ (impBracket premise.isImplicit $ - tidy premise.name) + show premise.name) , type = show premise.type } diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 1e68b0438..410c9d586 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -290,14 +290,15 @@ Cast REPLEval String where cast Scheme = "scheme" Cast REPLOpt REPLOption where - cast (ShowImplicits impl) = MkOption "show-implicits" BOOL impl - cast (ShowNamespace ns) = MkOption "show-namespace" BOOL ns - cast (ShowTypes typs) = MkOption "show-types" BOOL typs - cast (EvalMode mod) = MkOption "eval" ATOM $ cast mod - cast (Editor editor) = MkOption "editor" STRING editor - cast (CG str) = MkOption "cg" STRING str - cast (Profile p) = MkOption "profile" BOOL p - cast (EvalTiming p) = MkOption "evaltiming" BOOL p + cast (ShowImplicits impl) = MkOption "show-implicits" BOOL impl + cast (ShowNamespace ns) = MkOption "show-namespace" BOOL ns + cast (ShowMachineNames ns) = MkOption "show-machinenames" BOOL ns + cast (ShowTypes typs) = MkOption "show-types" BOOL typs + cast (EvalMode mod) = MkOption "eval" ATOM $ cast mod + cast (Editor editor) = MkOption "editor" STRING editor + cast (CG str) = MkOption "cg" STRING str + cast (Profile p) = MkOption "profile" BOOL p + cast (EvalTiming p) = MkOption "evaltiming" BOOL p displayIDEResult : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 90402523f..8bbb3265a 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -494,7 +494,7 @@ makeDoc pkg opts = Right () <- coreLift $ mkdirAll docDir | Left err => fileError docDir err u <- newRef UST initUState - setPPrint (MkPPOpts False False False) + setPPrint (MkPPOpts False True False False) [] <- concat <$> for (modules pkg) (\(mod, filename) => do -- load dependencies diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index dd2db1d73..c8c019e92 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1905,6 +1905,8 @@ setOption set pure (ShowImplicits set) <|> do exactIdent "shownamespace" pure (ShowNamespace set) + <|> do exactIdent "showmachinenames" + pure (ShowMachineNames set) <|> do exactIdent "showtypes" pure (ShowTypes set) <|> do exactIdent "profile" diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 5911a8bfa..c6874b520 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -101,16 +101,21 @@ showInfo (n, idx, d) "Size change: " ++ showSep ", " scinfo prettyInfo : {auto c : Ref Ctxt Defs} -> - (Name, Int, GlobalDef) -> Core (Doc IdrisDocAnn) + {auto s : Ref Syn SyntaxInfo} -> + (Name, Int, GlobalDef) -> Core (Doc IdrisDocAnn) prettyInfo (n, idx, d) = do let nm = fullname d def <- toFullNames (definition d) referCT <- traverse getFullName (keys (refersTo d)) referRT <- traverse getFullName (keys (refersToRuntime d)) schanges <- traverse toFullNames $ sizeChange d + pp <- getPPrint + setPPrint ({ showMachineNames := True } pp) + def <- Resugared.prettyDef def + setPPrint ({ showMachineNames := showMachineNames pp } pp) pure $ vcat $ [ reAnnotate Syntax (prettyRig $ multiplicity d) <+> showCategory Syntax d (pretty0 nm) - , pretty def + , def ] ++ catMaybes [ (\ args => header "Erasable args" <++> byShow args) <$> ifNotNull (eraseArgs d) @@ -162,6 +167,9 @@ setOpt (ShowImplicits t) setOpt (ShowNamespace t) = do pp <- getPPrint setPPrint ({ fullNamespace := t } pp) +setOpt (ShowMachineNames t) + = do pp <- getPPrint + setPPrint ({ showMachineNames := t } pp) setOpt (ShowTypes t) = update ROpts { showTypes := t } setOpt (EvalMode m) diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 0600d145c..088b1ac63 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -98,12 +98,6 @@ showFullEnv = do pp <- getPPrint pure (showFullEnv pp) -fullNamespace : {auto c : Ref Ctxt Defs} -> - Core Bool -fullNamespace - = do pp <- getPPrint - pure (fullNamespace pp) - unbracket : PTerm' nm -> PTerm' nm unbracket (PBracketed _ tm) = tm unbracket tm = tm @@ -111,11 +105,11 @@ unbracket tm = tm ||| Attempt to extract a constant natural number extractNat : Nat -> IPTerm -> Maybe Nat extractNat acc tm = case tm of - PRef _ (MkKindedName _ _ (NS ns (UN (Basic n)))) => + PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn) => do guard (n == "Z") guard (ns == typesNS || ns == preludeNS) pure acc - PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of + PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of "S" => do guard (ns == typesNS || ns == preludeNS) extractNat (1 + acc) k "fromInteger" => extractNat acc k @@ -128,7 +122,7 @@ extractNat acc tm = case tm of ||| Attempt to extract a constant integer extractInteger : IPTerm -> Maybe Integer extractInteger tm = case tm of - PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of + PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of "fromInteger" => extractInteger k "negate" => negate <$> extractInteger k _ => Nothing @@ -139,7 +133,7 @@ extractInteger tm = case tm of ||| Attempt to extract a constant double extractDouble : IPTerm -> Maybe Double extractDouble tm = case tm of - PApp _ (PRef _ (MkKindedName _ _ (NS ns (UN (Basic n))))) k => case n of + PApp _ (PRef _ (MkKindedName _ (NS ns (UN (Basic n))) rn)) k => case n of "fromDouble" => extractDouble k "negate" => negate <$> extractDouble k _ => Nothing @@ -152,11 +146,11 @@ mutual ||| Put the special names (Nil, ::, Pair, Z, S, etc) back as syntax ||| Returns `Nothing` in case there was nothing to resugar. sugarAppM : IPTerm -> Maybe IPTerm - sugarAppM (PApp fc (PApp _ (PApp _ (PRef opFC (MkKindedName nt _ (NS ns nm))) l) m) r) = + sugarAppM (PApp fc (PApp _ (PApp _ (PRef opFC (MkKindedName nt (NS ns nm) rn)) l) m) r) = case nameRoot nm of "rangeFromThenTo" => pure $ PRange fc (unbracket l) (Just $ unbracket m) (unbracket r) _ => Nothing - sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt _ (NS ns nm))) l) r) = + sugarAppM (PApp fc (PApp _ (PRef opFC (MkKindedName nt (NS ns nm) rn)) l) r) = if builtinNS == ns then case nameRoot nm of "Pair" => pure $ PPair fc (unbracket l) (unbracket r) @@ -189,7 +183,7 @@ mutual Nothing = extractDouble tm | Just d => pure $ PPrimVal (getPTermLoc tm) (Db d) in case tm of - PRef fc (MkKindedName nt _ (NS ns nm)) => + PRef fc (MkKindedName nt (NS ns nm) rn) => if builtinNS == ns then case nameRoot nm of "Unit" => pure $ PUnit fc @@ -199,7 +193,7 @@ mutual "Nil" => pure $ PList fc fc [] "Lin" => pure $ PSnocList fc fc [<] _ => Nothing - PApp fc (PRef _ (MkKindedName nt _ (NS ns nm))) arg => + PApp fc (PRef _ (MkKindedName nt (NS ns nm) rn)) arg => case nameRoot nm of "rangeFrom" => pure $ PRangeStream fc (unbracket arg) Nothing _ => Nothing @@ -218,12 +212,12 @@ sugarName (DN n _) = n sugarName x = show x toPRef : FC -> KindedName -> Core IPTerm -toPRef fc kn@(MkKindedName nt fn nm) = case nm of - MN n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n))) +toPRef fc (MkKindedName nt fn nm) = case dropNS nm of + MN n i => pure (sugarApp (PRef fc (MkKindedName nt fn $ MN n i))) PV n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ n))) DN n _ => pure (sugarApp (PRef fc (MkKindedName nt fn $ UN $ Basic n))) Nested _ n => toPRef fc (MkKindedName nt fn n) - _ => pure (sugarApp (PRef fc kn)) + n => pure (sugarApp (PRef fc (MkKindedName nt fn n))) mutual toPTerm : {auto c : Ref Ctxt Defs} -> @@ -524,17 +518,19 @@ export cleanPTerm : {auto c : Ref Ctxt Defs} -> IPTerm -> Core IPTerm cleanPTerm ptm - = do ns <- fullNamespace - if ns then pure ptm else mapPTermM cleanNode ptm + = do pp <- getPPrint + if showMachineNames pp then pure ptm else mapPTermM cleanNode ptm where cleanName : Name -> Core Name cleanName nm = case nm of - MN n _ => pure (UN $ mkUserName n) -- this may be "_" PV n _ => pure n - DN n _ => pure (UN $ mkUserName n) -- this may be "_" - NS _ n => cleanName n + -- Some of these may be "_" so we use `mkUserName` + MN n _ => pure (UN $ mkUserName n) + DN n _ => pure (UN $ mkUserName n) + -- namespaces have already been stripped in toPTerm if necessary + NS ns n => NS ns <$> cleanName n Nested _ n => cleanName n UN n => pure (UN n) _ => UN . mkUserName <$> prettyName nm diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 387721e6b..3874a5234 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -385,6 +385,14 @@ preOptions (Logging n :: opts) preOptions (ConsoleWidth n :: opts) = do setConsoleWidth n preOptions opts +preOptions (ShowMachineNames :: opts) + = do pp <- getPPrint + setPPrint ({ showMachineNames := True } pp) + preOptions opts +preOptions (ShowNamespaces :: opts) + = do pp <- getPPrint + setPPrint ({ fullNamespace := True } pp) + preOptions opts preOptions (Color b :: opts) = do setColor b preOptions opts diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index edc4a534f..fe22fd613 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -562,6 +562,7 @@ public export data REPLOpt : Type where ShowImplicits : Bool -> REPLOpt ShowNamespace : Bool -> REPLOpt + ShowMachineNames : Bool -> REPLOpt ShowTypes : Bool -> REPLOpt EvalMode : REPLEval -> REPLOpt Editor : String -> REPLOpt @@ -573,6 +574,7 @@ export Show REPLOpt where show (ShowImplicits impl) = "showimplicits = " ++ show impl show (ShowNamespace ns) = "shownamespace = " ++ show ns + show (ShowMachineNames mn) = "showmachinenames = " ++ show mn show (ShowTypes typs) = "showtypes = " ++ show typs show (EvalMode mod) = "eval = " ++ show mod show (Editor editor) = "editor = " ++ show editor @@ -582,14 +584,15 @@ Show REPLOpt where export Pretty Void REPLOpt where - pretty (ShowImplicits impl) = pretty "showimplicits" <++> equals <++> pretty (show impl) - pretty (ShowNamespace ns) = pretty "shownamespace" <++> equals <++> pretty (show ns) - pretty (ShowTypes typs) = pretty "showtypes" <++> equals <++> pretty (show typs) - pretty (EvalMode mod) = pretty "eval" <++> equals <++> pretty mod - pretty (Editor editor) = pretty "editor" <++> equals <++> pretty editor - pretty (CG str) = pretty "cg" <++> equals <++> pretty str - pretty (Profile p) = pretty "profile" <++> equals <++> pretty (show p) - pretty (EvalTiming p) = pretty "evaltiming" <++> equals <++> pretty (show p) + pretty (ShowImplicits impl) = "showimplicits" <++> equals <++> pretty (show impl) + pretty (ShowNamespace ns) = "shownamespace" <++> equals <++> pretty (show ns) + pretty (ShowMachineNames mn) = "showmachinenames" <++> equals <++> pretty (show mn) + pretty (ShowTypes typs) = "showtypes" <++> equals <++> pretty (show typs) + pretty (EvalMode mod) = "eval" <++> equals <++> pretty mod + pretty (Editor editor) = "editor" <++> equals <++> pretty editor + pretty (CG str) = "cg" <++> equals <++> pretty str + pretty (Profile p) = "profile" <++> equals <++> pretty (show p) + pretty (EvalTiming p) = "evaltiming" <++> equals <++> pretty (show p) public export data EditCmd : Type where diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index 627390be9..8bbb02e0f 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/src/Idris/Syntax/Traversals.idr @@ -23,9 +23,9 @@ mapPTermM f = goPTerm where <*> goPTerm argTy <*> goPTerm retTy >>= f - goPTerm (PLam fc x info z argTy scope) = + goPTerm (PLam fc x info pat argTy scope) = PLam fc x <$> goPiInfo info - <*> pure z + <*> goPTerm pat <*> goPTerm argTy <*> goPTerm scope >>= f diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 66c60d6a7..a4ba32d11 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -2,6 +2,7 @@ module TTImp.ProcessDef import Core.Case.CaseBuilder import Core.Case.CaseTree +import Core.Case.CaseTree.Pretty import Core.Context import Core.Context.Log import Core.Core @@ -804,11 +805,13 @@ mkRunTime fc n _ => clauses_init (rargs ** (tree_rt, _)) <- getPMDef (location gdef) RunTime n ty clauses - logC "compile.casetree" 5 $ pure $ unlines - [ show cov ++ ":" - , "Runtime tree for " ++ show (fullname gdef) ++ ":" - , show (indent 2 $ pretty !(toFullNames tree_rt)) - ] + logC "compile.casetree" 5 $ do + tree_rt <- toFullNames tree_rt + pure $ unlines + [ show cov ++ ":" + , "Runtime tree for " ++ show (fullname gdef) ++ ":" + , show (indent 2 $ prettyTree tree_rt) + ] log "compile.casetree" 10 $ show tree_rt log "compile.casetree.measure" 15 $ show (measure tree_rt) diff --git a/tests/Main.idr b/tests/Main.idr index 1b365b98b..4a1ffa61e 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -47,6 +47,10 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing "interpolation001", "interpolation002", "interpolation003", "interpolation004"] +idrisTestsDebug : TestPool +idrisTestsDebug = MkTestPool "Debug features" [] Nothing + ["debug001"] + idrisTestsCoverage : TestPool idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing -- Coverage checking @@ -96,7 +100,7 @@ idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing "interactive029", "interactive030", "interactive031", "interactive032", "interactive033", "interactive034", "interactive035", "interactive036", "interactive037", "interactive038", "interactive039", "interactive040", - "interactive041"] + "interactive041", "interactive042"] idrisTestsInterface : TestPool idrisTestsInterface = MkTestPool "Interface" [] Nothing @@ -362,6 +366,7 @@ main = runner $ , testPaths "idris2" idrisTestsSchemeEval , testPaths "idris2" idrisTestsReflection , testPaths "idris2" idrisTestsWith + , testPaths "idris2" idrisTestsDebug , testPaths "idris2" idrisTests , !typeddTests , !ideModeTests diff --git a/tests/idris2/basic023/expected b/tests/idris2/basic023/expected index 312474526..edb3231df 100644 --- a/tests/idris2/basic023/expected +++ b/tests/idris2/basic023/expected @@ -3,7 +3,7 @@ Main> Main.Dict : (a -> a -> Bool) -> Type -> Type Main> Main.MkDict : (eq : (a -> a -> Bool)) -> List (a, b) -> Dict eq b Main> Main.lookup : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b Main> Main.lookupK : (eq : (a -> a -> Bool)) -> a -> Dict eq b -> Maybe b -Main> MkDict (\{arg:0}, {arg:1} => intToBool (prim__eq_Int arg arg)) [(0, "foo"), (1, "bar")] +Main> MkDict (\arg, arg => intToBool (prim__eq_Int arg arg)) [(0, "foo"), (1, "bar")] Main> Just "bar" Main> Nothing Main> Bye for now! diff --git a/tests/idris2/coverage018/expected b/tests/idris2/coverage018/expected index 1e4939617..2aab32ecc 100644 --- a/tests/idris2/coverage018/expected +++ b/tests/idris2/coverage018/expected @@ -1,20 +1,20 @@ 1/1: Building Issue1831_1 (Issue1831_1.idr) Issue1831_1> Issue1831_1.test2 Arguments [{arg:0}] -Compile time tree: case {arg:0} : [__] of - Prelude.Types.S {e:0} => case {e:0} : [__] of - Prelude.Types.S {e:1} => case {e:1} : [__] of - Prelude.Types.Z => Prelude.Basics.True - _ => Prelude.Basics.False - _ => Prelude.Basics.False - _ => Prelude.Basics.False -Compiled: \ {arg:0} => case !{arg:0} of +Compile time tree: case {arg:0} of + S {e:0} => case {e:0} of + S {e:1} => case {e:1} of + Z => True + _ => False + _ => False + _ => False +Compiled: \ {arg:0} => case {arg:0} of { 0 => 0 - ; _ => let {e:0} = !{arg:0} - 1 in - case !{e:0} of + ; _ => let {e:0} = {arg:0} - 1 in + case {e:0} of { 0 => 0 - ; _ => let {e:1} = !{e:0} - 1 in - case !{e:1} of + ; _ => let {e:1} = {e:0} - 1 in + case {e:1} of { 0 => 1 ; _ => 0 } @@ -27,20 +27,20 @@ Bye for now! 1/1: Building Issue1831_2 (Issue1831_2.idr) Issue1831_2> Issue1831_2.test2 Arguments [{arg:0}] -Compile time tree: case {arg:0} : [__] of - Prelude.Types.S {e:0} => case {e:0} : [__] of - Prelude.Types.S {e:1} => case {e:1} : [__] of - Prelude.Types.Z => Prelude.Basics.True - _ => Prelude.Basics.False - _ => Prelude.Basics.False - _ => Prelude.Basics.False -Compiled: \ {arg:0} => case !{arg:0} of +Compile time tree: case {arg:0} of + S {e:0} => case {e:0} of + S {e:1} => case {e:1} of + Z => True + _ => False + _ => False + _ => False +Compiled: \ {arg:0} => case {arg:0} of { 0 => 0 - ; _ => let {e:0} = !{arg:0} - 1 in - case !{e:0} of + ; _ => let {e:0} = {arg:0} - 1 in + case {e:0} of { 0 => 0 - ; _ => let {e:1} = !{e:0} - 1 in - case !{e:1} of + ; _ => let {e:1} = {e:0} - 1 in + case {e:1} of { 0 => 1 ; _ => 0 } diff --git a/tests/idris2/debug001/TypePat.idr b/tests/idris2/debug001/TypePat.idr new file mode 100644 index 000000000..139759f70 --- /dev/null +++ b/tests/idris2/debug001/TypePat.idr @@ -0,0 +1,7 @@ +isNat : Type -> Bool +isNat Nat = True +isNat _ = False + +isInt32 : Type -> Bool +isInt32 Int32 = True +isInt32 _ = False diff --git a/tests/idris2/debug001/expected b/tests/idris2/debug001/expected new file mode 100644 index 000000000..3fbf5b785 --- /dev/null +++ b/tests/idris2/debug001/expected @@ -0,0 +1,81 @@ +1/1: Building TypePat (TypePat.idr) +Main> Main.isNat +Arguments [{arg:0}] +Compile time tree: case {arg:0} of + Nat => True + _ => False +Compiled: \ {arg:0} => case {arg:0} of + { Prelude.Types.Nat [tycon] => 1 + ; _ => 0 + } +Refers to: Prelude.Basics.True, Prelude.Basics.False +Flags: allguarded, covering +Main> Main.isInt32 +Arguments [{arg:0}] +Compile time tree: case {arg:0} of + Int32 => True + _ => False +Compiled: \ {arg:0} => case {arg:0} of + { Int32 [tycon] => 1 + ; _ => 0 + } +Refers to: Prelude.Basics.True, Prelude.Basics.False +Flags: allguarded, covering +Main> Prelude.Types.plus +Arguments [{arg:0}, {arg:1}] +Compile time tree: case {arg:0} of + Z => {arg:1} + S {e:0} => S (plus {e:0} {arg:1}) +Compiled: \ {arg:0}, {arg:1} => case {arg:0} of + { 0 => {arg:1} + ; _ => let {e:0} = {arg:0} - 1 in + ({e:0} + {arg:1}) + 1 + } +Refers to: Prelude.Types.plus, Prelude.Types.S +Flags: total +Size change: Prelude.Types.plus: [Just (0, Smaller), Just (1, Same)] +Main> Prelude.Types.minus +Arguments [{arg:0}, {arg:1}] +Compile time tree: case {arg:0} of + Z => 0 + _ => case {arg:1} of + Z => {arg:0} + _ => case {arg:0} of + S {e:0} => case {arg:1} of + S {e:1} => minus {e:0} {e:1} +Compiled: \ {arg:0}, {arg:1} => case {arg:0} of + { 0 => 0 + ; _ => case {arg:1} of + { 0 => {arg:0} + ; _ => case {arg:0} of + { 0 => crash "Nat case not covered" + ; _ => let {e:0} = {arg:0} - 1 in + case {arg:1} of + { 0 => crash "Nat case not covered" + ; _ => let {e:1} = {arg:1} - 1 in + Prelude.Types.prim__integerToNat ({e:0} - {e:1}) + } + } + } + } +Refers to: Prelude.Types.minus, Prelude.Types.Z +Refers to (runtime): Prelude.Types.prim__integerToNat +Flags: total +Size change: Prelude.Types.minus: [Just (0, Smaller), Just (1, Smaller)] +Main> Prelude.Types.SnocList.filter +Arguments [{arg:0}, {arg:1}, {arg:2}] +Compile time tree: case {arg:2} of + Lin {e:0} => [<] + (:<) {e:1} {e:2} {e:3} => let rest = filter {arg:1} {e:2} in if {arg:1} {e:3} then rest :< x else rest +Erasable args: [0] +Inferrable args: [0] +Compiled: \ {arg:1}, {arg:2} => case {arg:2} of + { Prelude.Basics.Lin {tag = 0} [nil] => Prelude.Basics.Lin {tag = 0} [nil] + ; Prelude.Basics.(:<) {tag = 1} [cons] {e:2} {e:3} => let rest = Prelude.Types.SnocList.filter {arg:1} {e:2} incase {arg:1} {e:3} of { 1 => Prelude.Basics.(:<) {tag = 1} [cons] rest {e:3}; 0 => rest} + } +Refers to: Prelude.Basics.SnocList, Prelude.Basics.Lin, Prelude.Types.SnocList.case block in filter, Prelude.Types.SnocList.filter +Refers to (runtime): Prelude.Basics.Lin, Prelude.Basics.(:<), Prelude.Types.SnocList.filter +Flags: total +Size change: Prelude.Types.SnocList.filter: [Just (0, Same), Just (1, Same), Just (2, Smaller)] +Main> +Bye for now! diff --git a/tests/idris2/debug001/input b/tests/idris2/debug001/input new file mode 100644 index 000000000..dde607f25 --- /dev/null +++ b/tests/idris2/debug001/input @@ -0,0 +1,6 @@ +:di isNat +:di isInt32 +:di plus +:di minus +:di SnocList.filter +:q \ No newline at end of file diff --git a/tests/idris2/debug001/run b/tests/idris2/debug001/run new file mode 100755 index 000000000..85fc0e384 --- /dev/null +++ b/tests/idris2/debug001/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner TypePat.idr < input diff --git a/tests/idris2/docs004/expected b/tests/idris2/docs004/expected index 03d9e53dc..52f04e73b 100644 --- a/tests/idris2/docs004/expected +++ b/tests/idris2/docs004/expected @@ -81,7 +81,7 @@ shiftR : Integer -> Index -> Integer shiftR x = prim__shr_Integer x . natToInteger bit : Index -> Integer -bit = \{arg:0} => 1 `shiftL` arg +bit = \arg => 1 `shiftL` arg zeroBits : Integer zeroBits = 0 diff --git a/tests/idris2/inlining001/expected b/tests/idris2/inlining001/expected index d2f5c7f44..118c7f2b5 100644 --- a/tests/idris2/inlining001/expected +++ b/tests/idris2/inlining001/expected @@ -1,39 +1,39 @@ 1/1: Building Inlining (Inlining.idr) Main> Main.leaveAlone Arguments [{arg:0}] -Compile time tree: (Prelude.Types.String.++ {arg:0}[0] "!") -Compiled: \ {arg:0} => !{arg:0} ++ "!" +Compile time tree: {arg:0} ++ "!" +Compiled: \ {arg:0} => {arg:0} ++ "!" Refers to: Prelude.Types.String.(++) Flags: covering Size change: Prelude.Types.String.(++): [Just (0, Same), Nothing] Main> Main.forceInline Arguments [{arg:0}] -Compile time tree: (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 {arg:0}[0] (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z))))))))))) -Compiled: \ {arg:0} => !{arg:0} + 10 +Compile time tree: {arg:0} + 10 +Compiled: \ {arg:0} => {arg:0} + 10 Refers to: Prelude.Types.Num implementation at Prelude.Types:66:1--71:33, Prelude.Types.Z, Prelude.Types.S, Prelude.Types.Nat, Prelude.Num.(+) Flags: covering, inline Size change: Prelude.Num.(+): [Nothing, Nothing, Just (0, Same), Nothing], Prelude.Types.Num implementation at Prelude.Types:66:1--71:33: [] Main> Main.forceNoInline Arguments [] -Compile time tree: (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))))))))) +Compile time tree: 10 Compiled: 10 Refers to: Prelude.Types.Z, Prelude.Types.S Flags: allguarded, covering, noinline Main> Main.heuristicPublicInline Arguments [] -Compile time tree: (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)) +Compile time tree: 2 Compiled: 2 Refers to: Prelude.Types.Z, Prelude.Types.S Flags: inline, allguarded, covering Main> Main.exportedForced Arguments [] -Compile time tree: (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z))))))))))))))))))))))))))))))))) +Compile time tree: 33 Compiled: 33 Refers to: Prelude.Types.Z, Prelude.Types.S Flags: allguarded, covering, inline Main> Main.exportedUnforced Arguments [] -Compile time tree: (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +Compile time tree: 66 Compiled: 66 Refers to: Prelude.Types.Z, Prelude.Types.S Flags: allguarded, covering diff --git a/tests/idris2/interactive042/Issue35-2.idr b/tests/idris2/interactive042/Issue35-2.idr new file mode 100644 index 000000000..7a63a1e9c --- /dev/null +++ b/tests/idris2/interactive042/Issue35-2.idr @@ -0,0 +1,4 @@ +f : { a, b : Type } -> Either a b -> Either b a +f {a=b} x = x +f (Right x) = Left x +f (Left x) = Right x diff --git a/tests/idris2/interactive042/Issue35.idr b/tests/idris2/interactive042/Issue35.idr new file mode 100644 index 000000000..dc46af0c2 --- /dev/null +++ b/tests/idris2/interactive042/Issue35.idr @@ -0,0 +1,10 @@ +test : {a : Nat} -> (b : Nat) -> a === b -> Nat +test a eq = ?a + +data Vect : Nat -> Type -> Type where + Nil : Vect 0 a + (::) : a -> Vect n a -> Vect (S n) a + +append : Vect n a -> Vect m a -> Vect (n + m) a +append [] ys = ys +append (x :: xs) ys = ?help diff --git a/tests/idris2/interactive042/expected b/tests/idris2/interactive042/expected new file mode 100644 index 000000000..22193ceab --- /dev/null +++ b/tests/idris2/interactive042/expected @@ -0,0 +1,63 @@ +1/1: Building Issue35 (Issue35.idr) +Main> a : Nat + eq : a = a +------------------------------ +a : Nat +Main> 0 m : Nat + 0 a : Type + x : a + xs : Vect n a + ys : Vect m a + 0 n : Nat +------------------------------ +help : Vect (S (plus n m)) a +Main> Main> a : Nat + eq : {a:827} = a +------------------------------ +a : Nat +Main> 0 m : Nat + 0 a : Type + x : a + xs : Vect {n:876} a + ys : Vect m a + 0 n : Nat +------------------------------ +help : Vect (S (plus {n:876} m)) a +Main> +Bye for now! +1/1: Building Issue35-2 (Issue35-2.idr) +Error: While processing right hand side of f. When unifying: + Either b b +and: + Either b b +Mismatch between: b (implicitly bound at Issue35-2:2:1--2:14) and b. + +Issue35-2:2:13--2:14 + 1 | f : { a, b : Type } -> Either a b -> Either b a + 2 | f {a=b} x = x + ^ + +1/1: Building Issue35-2 (Issue35-2.idr) +Error: While processing right hand side of f. When unifying: + Either b {b:826} +and: + Either {b:826} b +Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:14) and b. + +Issue35-2:2:13--2:14 + 1 | f : { a, b : Type } -> Either a b -> Either b a + 2 | f {a=b} x = x + ^ + +1/1: Building Issue35-2 (Issue35-2.idr) +Error: While processing right hand side of f. When unifying: + Prelude.Either b {b:826} +and: + Prelude.Either {b:826} b +Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:14) and b. + +Issue35-2:2:13--2:14 + 1 | f : { a, b : Type } -> Either a b -> Either b a + 2 | f {a=b} x = x + ^ + diff --git a/tests/idris2/interactive042/input b/tests/idris2/interactive042/input new file mode 100644 index 000000000..fc585e936 --- /dev/null +++ b/tests/idris2/interactive042/input @@ -0,0 +1,6 @@ +:t a +:t help +:set showmachinenames +:t a +:t help +:q \ No newline at end of file diff --git a/tests/idris2/interactive042/run b/tests/idris2/interactive042/run new file mode 100755 index 000000000..fa6424e48 --- /dev/null +++ b/tests/idris2/interactive042/run @@ -0,0 +1,6 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner Issue35.idr < input +$1 --no-color --console-width 0 --no-banner --check Issue35-2.idr || true +$1 --no-color --console-width 0 --no-banner --show-machine-names --check Issue35-2.idr || true +$1 --no-color --console-width 0 --no-banner --show-namespaces --show-machine-names --check Issue35-2.idr || true \ No newline at end of file diff --git a/tests/idris2/reg042/expected b/tests/idris2/reg042/expected index 7eea34904..78d1454e4 100644 --- a/tests/idris2/reg042/expected +++ b/tests/idris2/reg042/expected @@ -1,38 +1,38 @@ 1/1: Building NatOpts (NatOpts.idr) Main> Main.doPlus Arguments [{arg:0}, {arg:1}] -Compile time tree: (Prelude.Types.plus {arg:0}[0] {arg:1}[1]) -Compiled: \ {arg:0}, {arg:1} => !{arg:0} + !{arg:1} +Compile time tree: plus {arg:0} {arg:1} +Compiled: \ {arg:0}, {arg:1} => {arg:0} + {arg:1} Refers to: Prelude.Types.plus Flags: covering Size change: Prelude.Types.plus: [Just (0, Same), Just (1, Same)] Main> Main.doMinus Arguments [{arg:0}, {arg:1}] -Compile time tree: (Prelude.Types.minus {arg:0}[0] {arg:1}[1]) -Compiled: \ {arg:0}, {arg:1} => Prelude.Types.prim__integerToNat (!{arg:0} - !{arg:1}) +Compile time tree: minus {arg:0} {arg:1} +Compiled: \ {arg:0}, {arg:1} => Prelude.Types.prim__integerToNat ({arg:0} - {arg:1}) Refers to: Prelude.Types.minus Refers to (runtime): Prelude.Types.prim__integerToNat Flags: covering Size change: Prelude.Types.minus: [Just (0, Same), Just (1, Same)] Main> Main.doMult Arguments [{arg:0}, {arg:1}] -Compile time tree: (Prelude.Types.mult {arg:0}[0] {arg:1}[1]) -Compiled: \ {arg:0}, {arg:1} => !{arg:0} * !{arg:1} +Compile time tree: mult {arg:0} {arg:1} +Compiled: \ {arg:0}, {arg:1} => {arg:0} * {arg:1} Refers to: Prelude.Types.mult Flags: covering Size change: Prelude.Types.mult: [Just (0, Same), Just (1, Same)] Main> Main.doCompare Arguments [{arg:0}, {arg:1}] -Compile time tree: (Prelude.Types.compareNat {arg:0}[0] {arg:1}[1]) -Compiled: \ {arg:0}, {arg:1} => Prelude.EqOrd.compare !{arg:0} !{arg:1} +Compile time tree: compareNat {arg:0} {arg:1} +Compiled: \ {arg:0}, {arg:1} => Prelude.EqOrd.compare {arg:0} {arg:1} Refers to: Prelude.Types.compareNat Refers to (runtime): Prelude.EqOrd.compare Flags: covering Size change: Prelude.Types.compareNat: [Just (0, Same), Just (1, Same)] Main> Main.doEqual Arguments [{arg:0}, {arg:1}] -Compile time tree: (Prelude.Types.equalNat {arg:0}[0] {arg:1}[1]) -Compiled: \ {arg:0}, {arg:1} => !{arg:0} == !{arg:1} +Compile time tree: equalNat {arg:0} {arg:1} +Compiled: \ {arg:0}, {arg:1} => {arg:0} == {arg:1} Refers to: Prelude.Types.equalNat Flags: covering Size change: Prelude.Types.equalNat: [Just (0, Same), Just (1, Same)] diff --git a/tests/idris2/schemeeval003/expected b/tests/idris2/schemeeval003/expected index fc0cd676c..d693df4bf 100644 --- a/tests/idris2/schemeeval003/expected +++ b/tests/idris2/schemeeval003/expected @@ -1,3 +1,3 @@ -Main> [scheme] Main> 1 :: Delay (countFrom (1 + 1) (\{arg:0} => prim__add_Integer 1 arg)) +Main> [scheme] Main> 1 :: Delay (countFrom (1 + 1) (\arg => prim__add_Integer 1 arg)) [scheme] Main> [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] [scheme] Main> Bye for now! diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected index 406de3ec7..78a67d9ef 100644 --- a/tests/idris2/with003/expected +++ b/tests/idris2/with003/expected @@ -1,7 +1,7 @@ 1/1: Building Main (Main.idr) Main> Error: Ambiguous elaboration. Possible results: - Main.myPrintLn "foo" Prelude.(>>) Delay (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\{arg:0} => {arg:0} Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo"))) - Main.myPrintLn "foo" Main.Other.(>>) (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\{arg:0} => {arg:0} Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo"))) + Main.myPrintLn "foo" Prelude.(>>) Delay (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\arg => arg Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo"))) + Main.myPrintLn "foo" Main.Other.(>>) (Main.myPrintLn "boo" Main.Other.(>>) (Prelude.map (\arg => arg Prelude.(+) ?delayed) (Main.myPrintLn "woo") Main.Other.(>>) (Main.myPrintLn "goo" Main.Other.(>>) Main.myPrintLn "foo"))) (Interactive):1:4--1:19 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo"