mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 09:49:24 +03:00
Merge pull request #1354 from edwinb/casetransform
Add case+lambda transformation
This commit is contained in:
Edwin Brady
GitHub
commit
90ec19f053
@ -8,6 +8,7 @@ modules =
|
||||
Algebra.ZeroOneOmega,
|
||||
|
||||
Compiler.ANF,
|
||||
Compiler.CaseOpts,
|
||||
Compiler.Common,
|
||||
Compiler.CompileExpr,
|
||||
Compiler.Inline,
|
||||
|
||||
265
src/Compiler/CaseOpts.idr
Normal file
265
src/Compiler/CaseOpts.idr
Normal file
@ -0,0 +1,265 @@
|
||||
module Compiler.CaseOpts
|
||||
|
||||
-- Case block related transformations
|
||||
|
||||
import Compiler.CompileExpr
|
||||
|
||||
import Core.CompileExpr
|
||||
import Core.Context
|
||||
import Core.Context.Log
|
||||
import Core.FC
|
||||
import Core.TT
|
||||
|
||||
import Data.List
|
||||
import Data.Vect
|
||||
|
||||
%default covering
|
||||
|
||||
{-
|
||||
Lifting out lambdas:
|
||||
|
||||
case t of
|
||||
C1 => \x1 => e1
|
||||
...
|
||||
Cn => \xn = en
|
||||
|
||||
where every branch begins with a lambda, can become:
|
||||
|
||||
\x => case t of
|
||||
C1 => e1[x/x1]
|
||||
,,,
|
||||
Cn => en[x/xn]
|
||||
-}
|
||||
|
||||
shiftUnder : {args : _} ->
|
||||
{idx : _} ->
|
||||
(0 p : IsVar n idx (x :: args ++ vars)) ->
|
||||
NVar n (args ++ x :: vars)
|
||||
shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
|
||||
shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
|
||||
|
||||
shiftVar : {outer, args : _} ->
|
||||
{idx : _} ->
|
||||
(0 p : IsVar n idx (outer ++ (x :: args ++ vars))) ->
|
||||
NVar n (outer ++ (args ++ x :: vars))
|
||||
shiftVar {outer = []} p = shiftUnder p
|
||||
shiftVar {outer = (n::xs)} First = MkNVar First
|
||||
shiftVar {outer = (y::xs)} (Later p)
|
||||
= case shiftVar p of
|
||||
MkNVar p' => MkNVar (Later p')
|
||||
|
||||
mutual
|
||||
shiftBinder : {outer, args : _} ->
|
||||
(new : Name) ->
|
||||
CExp (outer ++ old :: (args ++ vars)) ->
|
||||
CExp (outer ++ (args ++ new :: vars))
|
||||
shiftBinder new (CLocal fc p)
|
||||
= case shiftVar p of
|
||||
MkNVar p' => CLocal fc (renameVar p')
|
||||
where
|
||||
renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->
|
||||
IsVar x i (outer ++ (args ++ (new :: rest)))
|
||||
renameVar = believe_me -- it's the same index, so just the identity at run time
|
||||
shiftBinder new (CRef fc n) = CRef fc n
|
||||
shiftBinder {outer} new (CLam fc n sc)
|
||||
= CLam fc n $ shiftBinder {outer = n :: outer} new sc
|
||||
shiftBinder new (CLet fc n inlineOK val sc)
|
||||
= CLet fc n inlineOK (shiftBinder new val)
|
||||
$ shiftBinder {outer = n :: outer} new sc
|
||||
shiftBinder new (CApp fc f args)
|
||||
= CApp fc (shiftBinder new f) $ map (shiftBinder new) args
|
||||
shiftBinder new (CCon fc c tag args)
|
||||
= CCon fc c tag $ map (shiftBinder new) args
|
||||
shiftBinder new (COp fc op args) = COp fc op $ map (shiftBinder new) args
|
||||
shiftBinder new (CExtPrim fc p args)
|
||||
= CExtPrim fc p $ map (shiftBinder new) args
|
||||
shiftBinder new (CForce fc r arg) = CForce fc r $ shiftBinder new arg
|
||||
shiftBinder new (CDelay fc r arg) = CDelay fc r $ shiftBinder new arg
|
||||
shiftBinder new (CConCase fc sc alts def)
|
||||
= CConCase fc (shiftBinder new sc)
|
||||
(map (shiftBinderConAlt new) alts)
|
||||
(map (shiftBinder new) def)
|
||||
shiftBinder new (CConstCase fc sc alts def)
|
||||
= CConstCase fc (shiftBinder new sc)
|
||||
(map (shiftBinderConstAlt new) alts)
|
||||
(map (shiftBinder new) def)
|
||||
shiftBinder new (CPrimVal fc c) = CPrimVal fc c
|
||||
shiftBinder new (CErased fc) = CErased fc
|
||||
shiftBinder new (CCrash fc msg) = CCrash fc msg
|
||||
|
||||
shiftBinderConAlt : {outer, args : _} ->
|
||||
(new : Name) ->
|
||||
CConAlt (outer ++ (x :: args ++ vars)) ->
|
||||
CConAlt (outer ++ (args ++ new :: vars))
|
||||
shiftBinderConAlt new (MkConAlt n t args' sc)
|
||||
= let sc' : CExp ((args' ++ outer) ++ (x :: args ++ vars))
|
||||
= rewrite sym (appendAssociative args' outer (x :: args ++ vars)) in sc in
|
||||
MkConAlt n t args' $
|
||||
rewrite (appendAssociative args' outer (args ++ new :: vars))
|
||||
in shiftBinder new {outer = args' ++ outer} sc'
|
||||
|
||||
shiftBinderConstAlt : {outer, args : _} ->
|
||||
(new : Name) ->
|
||||
CConstAlt (outer ++ (x :: args ++ vars)) ->
|
||||
CConstAlt (outer ++ (args ++ new :: vars))
|
||||
shiftBinderConstAlt new (MkConstAlt c sc) = MkConstAlt c $ shiftBinder new sc
|
||||
|
||||
-- If there's a lambda inside a case, move the variable so that it's bound
|
||||
-- outside the case block so that we can bind it just once outside the block
|
||||
liftOutLambda : {args : _} ->
|
||||
(new : Name) ->
|
||||
CExp (old :: args ++ vars) ->
|
||||
CExp (args ++ new :: vars)
|
||||
liftOutLambda = shiftBinder {outer = []}
|
||||
|
||||
-- If all the alternatives start with a lambda, we can have a single lambda
|
||||
-- binding outside
|
||||
tryLiftOut : (new : Name) ->
|
||||
List (CConAlt vars) ->
|
||||
Maybe (List (CConAlt (new :: vars)))
|
||||
tryLiftOut new [] = Just []
|
||||
tryLiftOut new (MkConAlt n t args (CLam fc x sc) :: as)
|
||||
= do as' <- tryLiftOut new as
|
||||
let sc' = liftOutLambda new sc
|
||||
pure (MkConAlt n t args sc' :: as')
|
||||
tryLiftOut _ _ = Nothing
|
||||
|
||||
tryLiftOutConst : (new : Name) ->
|
||||
List (CConstAlt vars) ->
|
||||
Maybe (List (CConstAlt (new :: vars)))
|
||||
tryLiftOutConst new [] = Just []
|
||||
tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
|
||||
= do as' <- tryLiftOutConst new as
|
||||
let sc' = liftOutLambda {args = []} new sc
|
||||
pure (MkConstAlt c sc' :: as')
|
||||
tryLiftOutConst _ _ = Nothing
|
||||
|
||||
tryLiftDef : (new : Name) ->
|
||||
Maybe (CExp vars) ->
|
||||
Maybe (Maybe (CExp (new :: vars)))
|
||||
tryLiftDef new Nothing = Just Nothing
|
||||
tryLiftDef new (Just (CLam fc x sc))
|
||||
= let sc' = liftOutLambda {args = []} new sc in
|
||||
pure (Just sc')
|
||||
tryLiftDef _ _ = Nothing
|
||||
|
||||
allLams : List (CConAlt vars) -> Bool
|
||||
allLams [] = True
|
||||
allLams (MkConAlt n t args (CLam _ _ _) :: as)
|
||||
= allLams as
|
||||
allLams _ = False
|
||||
|
||||
allLamsConst : List (CConstAlt vars) -> Bool
|
||||
allLamsConst [] = True
|
||||
allLamsConst (MkConstAlt c (CLam _ _ _) :: as)
|
||||
= allLamsConst as
|
||||
allLamsConst _ = False
|
||||
|
||||
-- label for next name for a lambda. These probably don't need really to be
|
||||
-- unique, since we've proved things about the de Bruijn index, but it's easier
|
||||
-- to see what's going on if they are.
|
||||
data NextName : Type where
|
||||
|
||||
getName : {auto n : Ref NextName Int} ->
|
||||
Core Name
|
||||
getName
|
||||
= do n <- get NextName
|
||||
put NextName (n + 1)
|
||||
pure (MN "clam" n)
|
||||
|
||||
-- The transformation itself
|
||||
mutual
|
||||
caseLam : {auto n : Ref NextName Int} ->
|
||||
CExp vars -> Core (CExp vars)
|
||||
-- Interesting cases first: look for case blocks where every branch is a
|
||||
-- lambda
|
||||
caseLam (CConCase fc sc alts def)
|
||||
= if allLams alts && defLam def
|
||||
then do var <- getName
|
||||
-- These will work if 'allLams' and 'defLam' are consistent.
|
||||
-- We only do that boolean check because it saves us doing
|
||||
-- unnecessary work (say, if the last one we try fails)
|
||||
let Just newAlts = tryLiftOut var alts
|
||||
| Nothing => throw (InternalError "Can't happen caseLam 1")
|
||||
let Just newDef = tryLiftDef var def
|
||||
| Nothing => throw (InternalError "Can't happen caseLam 2")
|
||||
newAlts' <- traverse caseLamConAlt newAlts
|
||||
newDef' <- traverseOpt caseLam newDef
|
||||
-- Q: Should we go around again?
|
||||
pure (CLam fc var (CConCase fc (weaken sc) newAlts' newDef'))
|
||||
else do sc' <- caseLam sc
|
||||
alts' <- traverse caseLamConAlt alts
|
||||
def' <- traverseOpt caseLam def
|
||||
pure (CConCase fc sc' alts' def')
|
||||
where
|
||||
defLam : Maybe (CExp vars) -> Bool
|
||||
defLam Nothing = True
|
||||
defLam (Just (CLam _ _ _)) = True
|
||||
defLam _ = False
|
||||
-- Next case is pretty much as above. There's a boring amount of repetition
|
||||
-- here because ConstCase is just a little bit different.
|
||||
caseLam (CConstCase fc sc alts def)
|
||||
= if allLamsConst alts && defLam def
|
||||
then do var <- getName
|
||||
-- These will work if 'allLams' and 'defLam' are consistent.
|
||||
-- We only do that boolean check because it saves us doing
|
||||
-- unnecessary work (say, if the last one we try fails)
|
||||
let Just newAlts = tryLiftOutConst var alts
|
||||
| Nothing => throw (InternalError "Can't happen caseLam 1")
|
||||
let Just newDef = tryLiftDef var def
|
||||
| Nothing => throw (InternalError "Can't happen caseLam 2")
|
||||
newAlts' <- traverse caseLamConstAlt newAlts
|
||||
newDef' <- traverseOpt caseLam newDef
|
||||
pure (CLam fc var (CConstCase fc (weaken sc) newAlts' newDef'))
|
||||
else do sc' <- caseLam sc
|
||||
alts' <- traverse caseLamConstAlt alts
|
||||
def' <- traverseOpt caseLam def
|
||||
pure (CConstCase fc sc' alts' def')
|
||||
where
|
||||
defLam : Maybe (CExp vars) -> Bool
|
||||
defLam Nothing = True
|
||||
defLam (Just (CLam _ _ _)) = True
|
||||
defLam _ = False
|
||||
-- Structural recursive cases
|
||||
caseLam (CLam fc x sc)
|
||||
= CLam fc x <$> caseLam sc
|
||||
caseLam (CLet fc x inl val sc)
|
||||
= CLet fc x inl <$> caseLam val <*> caseLam sc
|
||||
caseLam (CApp fc f args)
|
||||
= CApp fc <$> caseLam f <*> traverse caseLam args
|
||||
caseLam (CCon fc n t args)
|
||||
= CCon fc n t <$> traverse caseLam args
|
||||
caseLam (COp fc op args)
|
||||
= COp fc op <$> traverseVect caseLam args
|
||||
caseLam (CExtPrim fc p args)
|
||||
= CExtPrim fc p <$> traverse caseLam args
|
||||
caseLam (CForce fc r x)
|
||||
= CForce fc r <$> caseLam x
|
||||
caseLam (CDelay fc r x)
|
||||
= CDelay fc r <$> caseLam x
|
||||
-- All the others, no recursive case so just return the input
|
||||
caseLam x = pure x
|
||||
|
||||
caseLamConAlt : {auto n : Ref NextName Int} ->
|
||||
CConAlt vars -> Core (CConAlt vars)
|
||||
caseLamConAlt (MkConAlt n tag args sc)
|
||||
= MkConAlt n tag args <$> caseLam sc
|
||||
|
||||
caseLamConstAlt : {auto n : Ref NextName Int} ->
|
||||
CConstAlt vars -> Core (CConstAlt vars)
|
||||
caseLamConstAlt (MkConstAlt c sc) = MkConstAlt c <$> caseLam sc
|
||||
|
||||
export
|
||||
caseLamDef : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
caseLamDef n
|
||||
= do defs <- get Ctxt
|
||||
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
|
||||
let Just cexpr = compexpr def | Nothing => pure ()
|
||||
setCompiled n !(doCaseLam cexpr)
|
||||
where
|
||||
doCaseLam : CDef -> Core CDef
|
||||
doCaseLam (MkFun args def)
|
||||
= do n <- newRef NextName 0
|
||||
pure $ MkFun args !(caseLam def)
|
||||
doCaseLam d = pure d
|
||||
@ -1,5 +1,6 @@
|
||||
module Compiler.Inline
|
||||
|
||||
import Compiler.CaseOpts
|
||||
import Compiler.CompileExpr
|
||||
|
||||
import Core.CompileExpr
|
||||
@ -454,9 +455,12 @@ compileAndInlineAll
|
||||
|
||||
traverse_ inlineDef cns
|
||||
traverse_ mergeLamDef cns
|
||||
traverse_ caseLamDef cns
|
||||
traverse_ fixArityDef cns
|
||||
|
||||
traverse_ inlineDef cns
|
||||
traverse_ mergeLamDef cns
|
||||
traverse_ caseLamDef cns
|
||||
traverse_ fixArityDef cns
|
||||
where
|
||||
nonErased : Name -> Core Bool
|
||||
|
||||
@ -17,7 +17,7 @@ Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim_
|
||||
Prelude.Types.Z = Constructor tag Just 0 arity 0
|
||||
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Interfaces.pure = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} ((!{e:N} [___]) [!{arg:N}])))] Nothing)
|
||||
Prelude.Interfaces.pure = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
|
||||
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, ___, !{arg:N}])
|
||||
PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
|
||||
PrimIO.case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [___, ___, ___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{arg:N}])])
|
||||
|
||||
@ -16,7 +16,7 @@ prim__gt_Int = [{arg:N}, {arg:N}]: (>Int [!{arg:N}, !{arg:N}])
|
||||
prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
|
||||
prim__crash = [{arg:N}, {arg:N}]: (crash [!{arg:N}, !{arg:N}])
|
||||
prim__cast_IntegerInt = [{arg:N}]: (cast-Integer-Int [!{arg:N}])
|
||||
Main.main = [{ext:N}]: ((Prelude.Interfaces.sum [___, ___, (%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}])))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])])]) [(Prelude.Types.rangeFromTo [___, (%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
|
||||
Main.main = [{ext:N}]: (Prelude.Interfaces.sum [___, ___, (%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}])))]), (%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))])]), (Prelude.Types.rangeFromTo [___, (%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.div [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.mod [!{arg:N}, !{arg:N}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd./= [!{arg:N}, !{arg:N}])))]), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.compare [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.< [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.> [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.<= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.>= [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.max [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (Prelude.EqOrd.min [!{arg:N}, !{arg:N}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (+Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (*Int [!{arg:N}, !{arg:N}]))), (%lam {arg:N} (cast-Integer-Int [!{arg:N}]))]), (%lam {arg:N} (Prelude.Num.negate [!{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Num.- [!{arg:N}, !{arg:N}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
|
||||
Prelude.Basics.not = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 0)] Nothing)
|
||||
Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
|
||||
Prelude.Basics.True = Constructor tag Just 0 arity 0
|
||||
@ -50,7 +50,7 @@ Prelude.Types.Range implementation at Prelude/Types.idr:L:C--L:C = [{arg:N}, {ar
|
||||
Prelude.Types.Foldable implementation at Prelude/Types.idr:L:C--L:C = []: (%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam acc (%lam elem (%lam func (%lam init (%lam input (Prelude.Types.foldr [___, ___, !func, !init, !input])))))), (%lam elem (%lam acc (%lam func (%lam init (%lam input (Prelude.Types.foldl [___, ___, !func, !init, !input])))))), (%lam elem (%lam {arg:N} (Prelude.Types.null [___, !{arg:N}])))])
|
||||
Prelude.Types.takeUntil = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeUntil [___, !{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
|
||||
Prelude.Types.takeBefore = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Stream.:: Just 0 [{e:N}, {e:N}] (Prelude.Types.case block in takeBefore [___, !{e:N}, !{e:N}, !{arg:N}, (!{arg:N} [!{e:N}])]))] Nothing)
|
||||
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Types.prim__integerToNat = [{arg:N}]: (Prelude.Types.case block in prim__integerToNat [!{arg:N}, (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 1)] Just 0)])
|
||||
Prelude.Types.countFrom = [{arg:N}, {arg:N}, {arg:N}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [___, (!{arg:N} [!{arg:N}]), !{arg:N}]))])
|
||||
Prelude.Types.Z = Constructor tag Just 0 arity 0
|
||||
@ -74,9 +74,9 @@ Prelude.Num.Integral implementation at Prelude/Num.idr:L:C--L:C = []: (%con Prel
|
||||
Prelude.Num.- = [{ext:N}, {ext:N}]: (-Int [!{ext:N}, !{ext:N}])
|
||||
Prelude.Num.+ = [{ext:N}, {ext:N}]: (+Int [!{ext:N}, !{ext:N}])
|
||||
Prelude.Num.* = [{ext:N}, {ext:N}]: (*Int [!{ext:N}, !{ext:N}])
|
||||
Prelude.Num.fromInteger = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (!{e:N} [!{arg:N}])))] Nothing)
|
||||
Prelude.Num.- = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.Num.+ = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.Num.fromInteger = [{arg:N}, {arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [!{ext:N}]))] Nothing)
|
||||
Prelude.Num.- = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Num.+ = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.case block in case block in compare = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 1), (%constcase 1 2)] Nothing)
|
||||
Prelude.EqOrd.case block in compare = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 0), (%constcase 1 (Prelude.EqOrd.case block in case block in compare [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, !{arg:N}])]))] Nothing)
|
||||
Prelude.EqOrd.case block in max = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N}), (%constcase 1 !{arg:N})] Nothing)
|
||||
@ -98,18 +98,18 @@ Prelude.EqOrd./= = [{arg:N}, {arg:N}]: (Prelude.Basics.not [(Prelude.EqOrd.== [!
|
||||
Prelude.EqOrd.LT = Constructor tag Just 0 arity 0
|
||||
Prelude.EqOrd.GT = Constructor tag Just 2 arity 0
|
||||
Prelude.EqOrd.EQ = Constructor tag Just 1 arity 0
|
||||
Prelude.EqOrd.>= = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.EqOrd.> = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.EqOrd.<= = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.EqOrd.< = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)
|
||||
Prelude.EqOrd.>= = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.> = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.== = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.<= = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.EqOrd.< = [{arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}, {e:N}] ((!{e:N} [!{ext:N}]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Interfaces.sum = [{arg:N}, {arg:N}, {arg:N}]: (%case (Builtin.fst [___, ___, !{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [(%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} ((!{e:N} [!{arg:N}]) [!{arg:N}]))))] Nothing)]) [(%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{arg:N}])))] Nothing)
|
||||
Prelude.Interfaces.pure = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} ((!{e:N} [___]) [!{arg:N}])))] Nothing)
|
||||
Prelude.Interfaces.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{arg:N}]) [!{arg:N}]) [!{arg:N}])))))] Nothing)
|
||||
Prelude.Interfaces.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (%lam {arg:N} (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{arg:N}]) [!{arg:N}]) [!{arg:N}])))))] Nothing)
|
||||
Prelude.Interfaces.sum = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case (Builtin.fst [___, ___, !{arg:N}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {clam:N} (%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{clam:N}]))] Nothing)))]) [(%case (Builtin.snd [___, ___, !{arg:N}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Interfaces.pure = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [___]) [!{ext:N}]))] Nothing)
|
||||
Prelude.Interfaces.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
|
||||
Prelude.Interfaces.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}, {ext:N}]: (%case !{arg:N} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (%lam {arg:N} (((((!{e:N} [___]) [___]) [!{ext:N}]) [!{ext:N}]) [!{arg:N}])))] Nothing)
|
||||
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, ___, !{arg:N}])
|
||||
PrimIO.case block in case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (!{arg:N} [!{arg:N}])
|
||||
PrimIO.case block in io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (PrimIO.case block in case block in io_bind [___, ___, ___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{arg:N}])])
|
||||
|
||||
Loading…
Reference in New Issue
Block a user