mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-30 07:02:24 +03:00
[ doc ] prettier :di (#2356)
This commit is contained in:
G. Allais
GitHub
parent
fc38afc144
commit
0dfa7d8d79
@ -51,10 +51,12 @@ modules =
|
||||
Core.Case.CaseTree,
|
||||
Core.Case.Util,
|
||||
Core.CompileExpr,
|
||||
Core.CompileExpr.Pretty,
|
||||
Core.Context,
|
||||
Core.Context.Context,
|
||||
Core.Context.Data,
|
||||
Core.Context.Log,
|
||||
Core.Context.Pretty,
|
||||
Core.Core,
|
||||
Core.Coverage,
|
||||
Core.Directory,
|
||||
|
||||
154
src/Core/CompileExpr/Pretty.idr
Normal file
154
src/Core/CompileExpr/Pretty.idr
Normal file
@ -0,0 +1,154 @@
|
||||
module Core.CompileExpr.Pretty
|
||||
|
||||
import Core.Name
|
||||
import Core.CompileExpr
|
||||
import Core.TT
|
||||
import Data.List
|
||||
import Data.String
|
||||
import Data.Vect
|
||||
import Idris.Pretty
|
||||
import Libraries.Data.String.Extra
|
||||
|
||||
%default covering
|
||||
|
||||
export
|
||||
Pretty CFType where
|
||||
pretty = pretty . show
|
||||
|
||||
export
|
||||
Pretty LazyReason where
|
||||
pretty = pretty . show
|
||||
|
||||
|
||||
prettyFlag : ConInfo -> Doc ann
|
||||
prettyFlag DATACON = ""
|
||||
prettyFlag f = " [" <+> pretty (show f) <+> "]"
|
||||
|
||||
mutual
|
||||
export
|
||||
Pretty NamedCExp where
|
||||
prettyPrec d (NmLocal _ x) = "!" <+> pretty x
|
||||
prettyPrec d (NmRef _ x) = pretty x
|
||||
prettyPrec d (NmLam _ x y)
|
||||
= parenthesise (d > Open) $ "\\" <+> pretty x <+> "=>" <++> pretty y
|
||||
prettyPrec d (NmLet _ x y z) = vcat [ "let" <++> pretty x <++> "=" <++> pretty y <++> "in"
|
||||
, pretty z
|
||||
]
|
||||
prettyPrec d (NmApp _ x xs)
|
||||
= parenthesise (d > Open) $
|
||||
sep (pretty x :: map (prettyPrec App) xs)
|
||||
prettyPrec d (NmCon _ x ci tag xs)
|
||||
= parenthesise (d > Open) $
|
||||
sep (pretty x <+> braces ("tag =" <++> pretty tag) <+> prettyFlag ci
|
||||
:: map (prettyPrec App) xs)
|
||||
prettyPrec d (NmOp _ op xs)
|
||||
= parenthesise (d > Open) $ prettyOp op $ map (prettyPrec App) xs
|
||||
|
||||
where
|
||||
|
||||
prettyOp : PrimFn arity -> Vect arity (Doc ann) -> Doc ann
|
||||
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
|
||||
|
||||
prettyPrec d (NmExtPrim _ p xs)
|
||||
= parenthesise (d > Open) $
|
||||
sep (pretty p :: map (prettyPrec App) xs)
|
||||
prettyPrec d (NmForce _ lr x)
|
||||
= parenthesise (d > Open) $
|
||||
sep ["Force", prettyPrec App lr, prettyPrec App x]
|
||||
prettyPrec d (NmDelay _ lr x)
|
||||
= parenthesise (d > Open) $
|
||||
sep ["Delay", prettyPrec App lr, prettyPrec App x]
|
||||
prettyPrec d (NmConCase _ sc xs def)
|
||||
= parenthesise (d > Open) $ vcat
|
||||
(("case" <++> pretty sc <++> "of")
|
||||
:: zipWith (\ s, p => indent 2 $ s <++> pretty p)
|
||||
("{" :: (";" <$ xs))
|
||||
xs
|
||||
++ maybe [] (\ deflt => [indent 2 ("; _ =>" <+> softline <+> align (pretty deflt))]) def
|
||||
++ [indent 2 "}"])
|
||||
prettyPrec d (NmConstCase _ sc xs def)
|
||||
= parenthesise (d > Open) $ vcat
|
||||
(("case" <++> pretty sc <++> "of")
|
||||
:: zipWith (\ s, p => indent 2 $ s <++> pretty p)
|
||||
("{" :: (";" <$ xs))
|
||||
xs
|
||||
++ maybe [] (\ deflt => [indent 2 ("; _ =>" <+> softline <+> align (pretty deflt))]) def
|
||||
++ [indent 2 "}"])
|
||||
prettyPrec d (NmPrimVal _ x) = pretty x
|
||||
prettyPrec d (NmErased _) = "___"
|
||||
prettyPrec d (NmCrash _ x)
|
||||
= parenthesise (d > Open) $
|
||||
sep ["crash", prettyPrec App x]
|
||||
export
|
||||
Pretty NamedConAlt where
|
||||
pretty (MkNConAlt x ci tag args exp)
|
||||
= sep (pretty x <+> braces ("tag =" <++> pretty tag) <+> prettyFlag ci
|
||||
:: map (prettyPrec App) args
|
||||
++ ["=>" <+> softline <+> align (pretty exp) ])
|
||||
|
||||
export
|
||||
Pretty NamedConstAlt where
|
||||
pretty (MkNConstAlt x exp)
|
||||
= pretty x <++> "=>" <+> softline <+> align (pretty exp)
|
||||
|
||||
export
|
||||
{args : _} -> Pretty (CExp args) where
|
||||
pretty = pretty . forget
|
||||
|
||||
|
||||
export
|
||||
Pretty CDef where
|
||||
pretty (MkFun [] exp) = pretty exp
|
||||
pretty (MkFun args exp) =
|
||||
"\\" <++> concatWith (\ x, y => x <+> "," <++> y) (map pretty args)
|
||||
<++> "=>" <++> pretty exp
|
||||
pretty (MkCon mtag arity nt)
|
||||
= vcat $ (maybe "Data" (const "Type") mtag <++> "Constructor:") :: map (indent 2)
|
||||
( maybe [] (\ tag => ["tag:" <++> pretty tag]) mtag ++
|
||||
[ "arity:" <++> pretty arity ] ++
|
||||
maybe [] (\ n => ["newtype by:" <++> pretty n]) nt)
|
||||
pretty (MkForeign ccs args ret)
|
||||
= vcat $ "Foreign function:" :: map (indent 2)
|
||||
[ "bindings:" <++> pretty ccs
|
||||
, "argument types:" <++> pretty args
|
||||
, "return type:" <++> pretty ret
|
||||
]
|
||||
pretty (MkError exp) = "Error:" <++> pretty exp
|
||||
@ -8,6 +8,7 @@ import public Core.Options.Log
|
||||
import public Core.TT
|
||||
|
||||
import Data.IORef
|
||||
import Data.String
|
||||
|
||||
import Libraries.Data.IntMap
|
||||
import Libraries.Data.IOArray
|
||||
@ -139,8 +140,10 @@ covering
|
||||
Show Def where
|
||||
show None = "undefined"
|
||||
show (PMDef _ args ct rt pats)
|
||||
= show args ++ ";\nCompile time tree: " ++ show ct ++
|
||||
"\nRun time tree: " ++ show rt
|
||||
= unlines [ show args ++ ";"
|
||||
, "Compile time tree: " ++ show ct
|
||||
, "Run time tree: " ++ show rt
|
||||
]
|
||||
show (DCon t a nt)
|
||||
= "DataCon " ++ show t ++ " " ++ show a
|
||||
++ maybe "" (\n => " (newtype by " ++ show n ++ ")") nt
|
||||
|
||||
57
src/Core/Context/Pretty.idr
Normal file
57
src/Core/Context/Pretty.idr
Normal file
@ -0,0 +1,57 @@
|
||||
module Core.Context.Pretty
|
||||
|
||||
import Data.String
|
||||
import Idris.Pretty
|
||||
|
||||
import Core.Case.CaseTree
|
||||
import Core.Context.Context
|
||||
|
||||
import Libraries.Data.String.Extra
|
||||
|
||||
%default covering
|
||||
|
||||
export
|
||||
Pretty Def where
|
||||
pretty None = "undefined"
|
||||
pretty (PMDef _ args ct _ pats)
|
||||
= vcat [ "Arguments" <++> pretty args
|
||||
, "Compile time tree:" <++> pretty ct
|
||||
]
|
||||
pretty (DCon tag arity nt)
|
||||
= vcat $ "Data constructor:" :: map (indent 2)
|
||||
([ "tag:" <++> pretty tag
|
||||
, "arity:" <++> pretty arity
|
||||
] ++ maybe [] (\ n => ["newtype by:" <++> pretty n]) nt)
|
||||
pretty (TCon tag arity ps ds u ms cons det)
|
||||
= vcat $ "Type constructor:" :: map (indent 2)
|
||||
([ "tag:" <++> pretty tag
|
||||
, "arity:" <++> pretty arity
|
||||
, "parameter positions:" <++> pretty ps
|
||||
, "constructors:" <++> pretty cons
|
||||
] ++ (("mutual with:" <++> pretty ms) <$ guard (not $ null ms))
|
||||
++ (maybe [] (\ pos => ["detaggable by:" <++> pretty pos]) det))
|
||||
pretty (ExternDef arity)
|
||||
= vcat $ "External definition:" :: map (indent 2)
|
||||
[ "arity:" <++> pretty arity ]
|
||||
pretty (ForeignDef arity calls)
|
||||
= vcat $ "Foreign definition:" :: map (indent 2)
|
||||
[ "arity:" <++> pretty arity
|
||||
, "bindings:" <++> pretty calls ]
|
||||
pretty (Builtin {arity} _)
|
||||
= vcat $ "Builtin:" :: map (indent 2)
|
||||
[ "arity:" <++> pretty arity ]
|
||||
pretty (Hole numlocs hf)
|
||||
= vcat $ "Hole:" :: map (indent 2)
|
||||
("Implicitly bound name" <$ guard (implbind hf))
|
||||
pretty (BySearch rig depth def)
|
||||
= vcat $ "Search:" :: map (indent 2)
|
||||
[ "depth:" <++> pretty depth
|
||||
, "in:" <++> pretty def ]
|
||||
pretty (Guess tm _ cs)
|
||||
= vcat $ "Guess:" :: map (indent 2)
|
||||
[ "solution:" <++> pretty tm
|
||||
, "when:" <++> pretty cs ]
|
||||
pretty (UniverseLevel i)
|
||||
= "Universe level #" <+> pretty i
|
||||
pretty ImpBind = "Bound name"
|
||||
pretty Delayed = "Delayed"
|
||||
@ -5,8 +5,10 @@ import Compiler.Inline
|
||||
|
||||
import Core.Case.CaseTree
|
||||
import Core.CompileExpr
|
||||
import Core.CompileExpr.Pretty
|
||||
import Core.Context
|
||||
import Core.Context.Log
|
||||
import Core.Context.Pretty
|
||||
import Core.Directory
|
||||
import Core.Env
|
||||
import Core.FC
|
||||
@ -72,6 +74,8 @@ import System.File
|
||||
|
||||
%default covering
|
||||
|
||||
-- Do NOT remove: it can be used instead of prettyInfo in case the prettier output
|
||||
-- happens to be buggy
|
||||
showInfo : {auto c : Ref Ctxt Defs} ->
|
||||
(Name, Int, GlobalDef) -> Core ()
|
||||
showInfo (n, idx, d)
|
||||
@ -95,6 +99,43 @@ showInfo (n, idx, d)
|
||||
coreLift_ $ putStrLn $
|
||||
"Size change: " ++ showSep ", " scinfo
|
||||
|
||||
prettyInfo : {auto c : Ref Ctxt Defs} ->
|
||||
(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
|
||||
pure $ vcat $
|
||||
[ reAnnotate Syntax (prettyRig $ multiplicity d) <+> showCategory Syntax d (pretty nm)
|
||||
, pretty def
|
||||
] ++
|
||||
catMaybes
|
||||
[ (\ args => header "Erasable args" <++> pretty args) <$> ifNotNull (eraseArgs d)
|
||||
, (\ args => header "Detaggable arg types" <++> pretty args) <$> ifNotNull (safeErase d)
|
||||
, (\ args => header "Specialise args" <++> pretty args) <$> ifNotNull (specArgs d)
|
||||
, (\ args => header "Inferrable args" <++> pretty args) <$> ifNotNull (inferrable d)
|
||||
, (\ expr => header "Compiled" <++> pretty expr) <$> compexpr d
|
||||
, (\ nms => header "Refers to" <++> enum pretty nms) <$> ifNotNull referCT
|
||||
, (\ nms => header "Refers to (runtime)" <++> enum pretty nms) <$> ifNotNull referRT
|
||||
, (\ flgs => header "Flags" <++> enum (pretty . show) flgs) <$> ifNotNull (flags d)
|
||||
, (\ sz => header "Size change" <++> displayChg sz) <$> ifNotNull schanges
|
||||
]
|
||||
|
||||
where
|
||||
ifNotNull : List a -> Maybe (List a)
|
||||
ifNotNull xs = xs <$ guard (not $ null xs)
|
||||
|
||||
enum : (a -> Doc IdrisDocAnn) -> List a -> Doc IdrisDocAnn
|
||||
enum p xs = hsep $ punctuate "," $ p <$> xs
|
||||
|
||||
displayChg : List SCCall -> Doc IdrisDocAnn
|
||||
displayChg sz =
|
||||
let scinfo = \s => pretty (fnCall s) <+> ":" <++> pretty (show $ fnArgs s) in
|
||||
enum scinfo sz
|
||||
|
||||
|
||||
prettyTerm : IPTerm -> Doc IdrisAnn
|
||||
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm
|
||||
|
||||
@ -853,8 +894,8 @@ process (Browse ns)
|
||||
pure $ PrintedDoc doc
|
||||
process (DebugInfo n)
|
||||
= do defs <- get Ctxt
|
||||
traverse_ showInfo !(lookupCtxtName n (gamma defs))
|
||||
pure Done
|
||||
ds <- traverse prettyInfo !(lookupCtxtName n (gamma defs))
|
||||
pure $ PrintedDoc $ vcat $ punctuate hardline ds
|
||||
process (SetOpt opt)
|
||||
= do setOpt opt
|
||||
pure Done
|
||||
|
||||
@ -1,22 +1,20 @@
|
||||
1/1: Building Main (Main.idr)
|
||||
Main> Main.MkFoo ==> DataCon 0 1 (newtype by (False, 0))
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: Constructor tag Just 0 arity 1 (newtype by 0)
|
||||
Refers to: []
|
||||
Refers to (runtime): []
|
||||
Flags: [contype [record]]
|
||||
Main> Main.MkBar ==> DataCon 0 1
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: Constructor tag Just 0 arity 1
|
||||
Refers to: []
|
||||
Refers to (runtime): []
|
||||
Flags: [contype [record]]
|
||||
Main> Main.MkFoo
|
||||
Data constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
newtype by: (False, 0)
|
||||
Compiled: Type Constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
newtype by: 0
|
||||
Flags: contype [record]
|
||||
Main> Main.MkBar
|
||||
Data constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
Compiled: Type Constructor:
|
||||
tag: 0
|
||||
arity: 1
|
||||
Flags: contype [record]
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,48 +1,52 @@
|
||||
1/1: Building Issue1831_1 (Issue1831_1.idr)
|
||||
Issue1831_1> Issue1831_1.test2 ==> [{arg:0}];
|
||||
Compile time tree: case {arg:0}[0] : [__] of
|
||||
{ Prelude.Types.S {e:0} => case {e:0}[0] : [__] of
|
||||
{ Prelude.Types.S {e:1} => case {e:1}[0] : [__] of
|
||||
{ Prelude.Types.Z => [0] Prelude.Basics.True
|
||||
| _ => [0] Prelude.Basics.False
|
||||
}
|
||||
| _ => [0] Prelude.Basics.False
|
||||
}
|
||||
| _ => [0] Prelude.Basics.False
|
||||
}
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}]: (%case !{arg:0} [(%constcase 0 0)] Just (%let {e:0} (-Integer [!{arg:0}, 1]) (%case !{e:0} [(%constcase 0 0)] Just (%let {e:1} (-Integer [!{e:0}, 1]) (%case !{e:1} [(%constcase 0 1)] Just 0)))))
|
||||
Refers to: [Prelude.Basics.True, Prelude.Basics.False]
|
||||
Refers to (runtime): []
|
||||
Flags: [allguarded, covering]
|
||||
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
|
||||
{ 0 => 0
|
||||
; _ => let {e:0} = !{arg:0} - 1 in
|
||||
case !{e:0} of
|
||||
{ 0 => 0
|
||||
; _ => let {e:1} = !{e:0} - 1 in
|
||||
case !{e:1} of
|
||||
{ 0 => 1
|
||||
; _ => 0
|
||||
}
|
||||
}
|
||||
}
|
||||
Refers to: Prelude.Basics.True, Prelude.Basics.False
|
||||
Flags: allguarded, covering
|
||||
Issue1831_1>
|
||||
Bye for now!
|
||||
1/1: Building Issue1831_2 (Issue1831_2.idr)
|
||||
Issue1831_2> Issue1831_2.test2 ==> [{arg:0}];
|
||||
Compile time tree: case {arg:0}[0] : [__] of
|
||||
{ Prelude.Types.S {e:0} => case {e:0}[0] : [__] of
|
||||
{ Prelude.Types.S {e:1} => case {e:1}[0] : [__] of
|
||||
{ Prelude.Types.Z => [0] Prelude.Basics.True
|
||||
| _ => [0] Prelude.Basics.False
|
||||
}
|
||||
| _ => [0] Prelude.Basics.False
|
||||
}
|
||||
| _ => [0] Prelude.Basics.False
|
||||
}
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}]: (%case !{arg:0} [(%constcase 0 0)] Just (%let {e:0} (-Integer [!{arg:0}, 1]) (%case !{e:0} [(%constcase 0 0)] Just (%let {e:1} (-Integer [!{e:0}, 1]) (%case !{e:1} [(%constcase 0 1)] Just 0)))))
|
||||
Refers to: [Prelude.Basics.True, Prelude.Basics.False]
|
||||
Refers to (runtime): []
|
||||
Flags: [allguarded, covering]
|
||||
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
|
||||
{ 0 => 0
|
||||
; _ => let {e:0} = !{arg:0} - 1 in
|
||||
case !{e:0} of
|
||||
{ 0 => 0
|
||||
; _ => let {e:1} = !{e:0} - 1 in
|
||||
case !{e:1} of
|
||||
{ 0 => 1
|
||||
; _ => 0
|
||||
}
|
||||
}
|
||||
}
|
||||
Refers to: Prelude.Basics.True, Prelude.Basics.False
|
||||
Flags: allguarded, covering
|
||||
Issue1831_2>
|
||||
Bye for now!
|
||||
|
||||
@ -1,76 +1,40 @@
|
||||
1/1: Building Inlining (Inlining.idr)
|
||||
Main> Main.leaveAlone ==> [{arg:0}];
|
||||
Compile time tree: [0] (Prelude.Types.String.++ {arg:0}[0] "!")
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}]: (++ [!{arg:0}, "!"])
|
||||
Refers to: [Prelude.Types.String.++]
|
||||
Refers to (runtime): []
|
||||
Flags: [covering]
|
||||
Size change: Prelude.Types.String.++: [Just (0, Same), Nothing]
|
||||
Main> Main.forceInline ==> [{arg:0}];
|
||||
Compile time tree: [0] (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)))))))))))
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}]: (+Integer [!{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.+]
|
||||
Refers to (runtime): []
|
||||
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 ==> [];
|
||||
Compile time tree: [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))))))))))
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: []: 10
|
||||
Refers to: [Prelude.Types.Z, Prelude.Types.S]
|
||||
Refers to (runtime): []
|
||||
Flags: [allguarded, covering, noinline]
|
||||
Main> Main.heuristicPublicInline ==> [];
|
||||
Compile time tree: [0] (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z))
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: []: 2
|
||||
Refers to: [Prelude.Types.Z, Prelude.Types.S]
|
||||
Refers to (runtime): []
|
||||
Flags: [inline, allguarded, covering]
|
||||
Main> Main.exportedForced ==> [];
|
||||
Compile time tree: [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.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)))))))))))))))))))))))))))))))))
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: []: 33
|
||||
Refers to: [Prelude.Types.Z, Prelude.Types.S]
|
||||
Refers to (runtime): []
|
||||
Flags: [allguarded, covering, inline]
|
||||
Main> Main.exportedUnforced ==> [];
|
||||
Compile time tree: [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.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: []: 66
|
||||
Refers to: [Prelude.Types.Z, Prelude.Types.S]
|
||||
Refers to (runtime): []
|
||||
Flags: [allguarded, covering]
|
||||
Main> Main.leaveAlone
|
||||
Arguments [{arg:0}]
|
||||
Compile time tree: (Prelude.Types.String.++ {arg:0}[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
|
||||
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))))))))))
|
||||
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))
|
||||
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)))))))))))))))))))))))))))))))))
|
||||
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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
Compiled: 66
|
||||
Refers to: Prelude.Types.Z, Prelude.Types.S
|
||||
Flags: allguarded, covering
|
||||
Main> Bye for now!
|
||||
|
||||
@ -1,67 +1,39 @@
|
||||
1/1: Building NatOpts (NatOpts.idr)
|
||||
Main> Main.doPlus ==> [{arg:0}, {arg:1}];
|
||||
Compile time tree: [0] (Prelude.Types.plus {arg:0}[0] {arg:1}[1])
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}, {arg:1}]: (+Integer [!{arg:0}, !{arg:1}])
|
||||
Refers to: [Prelude.Types.plus]
|
||||
Refers to (runtime): []
|
||||
Flags: [covering]
|
||||
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}
|
||||
Refers to: Prelude.Types.plus
|
||||
Flags: covering
|
||||
Size change: Prelude.Types.plus: [Just (0, Same), Just (1, Same)]
|
||||
Main> Main.doMinus ==> [{arg:0}, {arg:1}];
|
||||
Compile time tree: [0] (Prelude.Types.minus {arg:0}[0] {arg:1}[1])
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}, {arg:1}]: (Prelude.Types.prim__integerToNat [(-Integer [!{arg:0}, !{arg:1}])])
|
||||
Refers to: [Prelude.Types.minus]
|
||||
Refers to (runtime): [Prelude.Types.prim__integerToNat]
|
||||
Flags: [covering]
|
||||
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})
|
||||
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 ==> [{arg:0}, {arg:1}];
|
||||
Compile time tree: [0] (Prelude.Types.mult {arg:0}[0] {arg:1}[1])
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}, {arg:1}]: (*Integer [!{arg:0}, !{arg:1}])
|
||||
Refers to: [Prelude.Types.mult]
|
||||
Refers to (runtime): []
|
||||
Flags: [covering]
|
||||
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}
|
||||
Refers to: Prelude.Types.mult
|
||||
Flags: covering
|
||||
Size change: Prelude.Types.mult: [Just (0, Same), Just (1, Same)]
|
||||
Main> Main.doCompare ==> [{arg:0}, {arg:1}];
|
||||
Compile time tree: [0] (Prelude.Types.compareNat {arg:0}[0] {arg:1}[1])
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
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]
|
||||
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}
|
||||
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 ==> [{arg:0}, {arg:1}];
|
||||
Compile time tree: [0] (Prelude.Types.equalNat {arg:0}[0] {arg:1}[1])
|
||||
Run time tree: Error: ""
|
||||
RigW
|
||||
Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: [{arg:0}, {arg:1}]: (==Integer [!{arg:0}, !{arg:1}])
|
||||
Refers to: [Prelude.Types.equalNat]
|
||||
Refers to (runtime): []
|
||||
Flags: [covering]
|
||||
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}
|
||||
Refers to: Prelude.Types.equalNat
|
||||
Flags: covering
|
||||
Size change: Prelude.Types.equalNat: [Just (0, Same), Just (1, Same)]
|
||||
Main> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user