mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-28 11:05:17 +03:00
Add Agda-like builtins (#1253)
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
This commit is contained in:
Zoe Stafford
GitHub
parent
181b26b250
commit
c75b3f7f14
72
docs/source/reference/builtins.rst
Normal file
72
docs/source/reference/builtins.rst
Normal file
@ -0,0 +1,72 @@
|
||||
********
|
||||
Builtins
|
||||
********
|
||||
|
||||
.. role:: idris(code)
|
||||
:language: idris
|
||||
|
||||
Idris2 supports an optimised runtime representation of some types,
|
||||
using the ``%builtin`` pragma.
|
||||
For now only ``Nat``-like types has been implemented.
|
||||
|
||||
``%builtin Natural``
|
||||
====================
|
||||
|
||||
I suggest having a look at the source for ``Nat`` (in ``Prelude.Types``) before reading this section.
|
||||
|
||||
The ``%builtin Natural`` pragma converts recursive/unary representations of natural numbers
|
||||
into primitive ``Integer`` representations.
|
||||
This massively reduces the memory usage and offers a small speed improvement,
|
||||
for example with the unary representation ``the Nat 1000`` would take up about 2000 * 8 bytes
|
||||
(1000 for the tag, 1000 for the pointers) whereas the ``Integer`` representation takes about 8 to 16 bytes.
|
||||
|
||||
Here's an example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Nat
|
||||
= Z
|
||||
| S Nat
|
||||
|
||||
%builtin Natural Nat
|
||||
|
||||
Note that the order of the constructors doesn't matter.
|
||||
Furthermore this pragma supports GADTs
|
||||
so long as any extra arguments are erased.
|
||||
|
||||
For example:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data Fin : Nat -> Type where
|
||||
FZ : Fin (S k)
|
||||
FS : Fin k -> Fin (S k)
|
||||
|
||||
%builtin Natural Fin
|
||||
|
||||
works because the ``k`` is always erased.
|
||||
|
||||
This doesn't work if the argument to the ``S``-like constructor
|
||||
is ``Inf`` (sometime known as ``CoNat``) as these can be infinite
|
||||
or is ``Lazy`` as it wouldn't preserve laziness semantics.
|
||||
|
||||
During codegen any occurance of ``Nat`` will be converted to the faster ``Integer`` implementation.
|
||||
Here are the specifics for the conversion:
|
||||
|
||||
``Z`` => ``0``
|
||||
|
||||
``S k`` => ``1 + k``
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
case k of
|
||||
Z => zexp
|
||||
S k' => sexp
|
||||
|
||||
=>
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
case k of
|
||||
0 => zexp
|
||||
_ => let k' = k - 1 in sexp
|
||||
@ -21,3 +21,4 @@ This is a placeholder, to get set up with readthedocs.
|
||||
records
|
||||
literate
|
||||
overloadedlit
|
||||
builtins
|
||||
|
||||
@ -173,6 +173,7 @@ modules =
|
||||
TTImp.Impossible,
|
||||
TTImp.Parser,
|
||||
TTImp.PartialEval,
|
||||
TTImp.ProcessBuiltin,
|
||||
TTImp.ProcessData,
|
||||
TTImp.ProcessDecls,
|
||||
TTImp.ProcessDef,
|
||||
|
||||
@ -127,7 +127,7 @@ mkDropSubst i es rest (x :: xs)
|
||||
then (vs ** DropCons sub)
|
||||
else (x :: vs ** KeepCons sub)
|
||||
|
||||
-- Rewrite applications of Nat constructors and functions to more optimal
|
||||
-- Rewrite applications of Nat-like constructors and functions to more optimal
|
||||
-- versions using Integer
|
||||
|
||||
-- None of these should be hard coded, but we'll do it this way until we
|
||||
@ -136,10 +136,10 @@ mkDropSubst i es rest (x :: xs)
|
||||
-- Common.idr, so that they get compiled, as they won't be spotted by the
|
||||
-- usual calls to 'getRefs'.
|
||||
data Magic : Type where
|
||||
MagicCCon : Namespace -> String -> (arity : Nat) -> -- checks
|
||||
MagicCCon : Name -> (arity : Nat) -> -- checks
|
||||
(FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> -- translation
|
||||
Magic
|
||||
MagicCRef : Namespace -> String -> (arity : Nat) -> -- checks
|
||||
MagicCRef : Name -> (arity : Nat) -> -- checks
|
||||
(FC -> FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> --translation
|
||||
Magic
|
||||
|
||||
@ -148,11 +148,11 @@ magic ms (CLam fc x exp) = CLam fc x (magic ms exp)
|
||||
magic ms e = go ms e where
|
||||
|
||||
fire : Magic -> CExp vars -> Maybe (CExp vars)
|
||||
fire (MagicCCon ns n arity f) (CCon fc (NS ns' (UN n')) _ es)
|
||||
= do guard (n == n' && ns == ns')
|
||||
fire (MagicCCon n arity f) (CCon fc n' _ es)
|
||||
= do guard (n == n')
|
||||
map (f fc) (toVect arity es)
|
||||
fire (MagicCRef ns n arity f) (CApp fc (CRef fc' (NS ns' (UN n'))) es)
|
||||
= do guard (n == n' && ns == ns')
|
||||
fire (MagicCRef n arity f) (CApp fc (CRef fc' n') es)
|
||||
= do guard (n == n')
|
||||
map (f fc fc') (toVect arity es)
|
||||
fire _ _ = Nothing
|
||||
|
||||
@ -165,63 +165,99 @@ magic ms e = go ms e where
|
||||
natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
|
||||
natMinus fc fc' [m,n] = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]
|
||||
|
||||
natHack : CExp vars -> CExp vars
|
||||
natHack = magic
|
||||
[ MagicCCon typesNS "Z" 0
|
||||
(\ fc, [] => CPrimVal fc (BI 0))
|
||||
, MagicCCon typesNS "S" 1
|
||||
(\ fc, [k] => CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k])
|
||||
, MagicCRef typesNS "natToInteger" 1
|
||||
-- TODO: next release remove this and use %builtin pragma
|
||||
natHack : List Magic
|
||||
natHack =
|
||||
[ MagicCRef (NS typesNS (UN "natToInteger")) 1
|
||||
(\ _, _, [k] => k)
|
||||
, MagicCRef typesNS "integerToNat" 1
|
||||
, MagicCRef (NS typesNS (UN "integerToNat")) 1
|
||||
(\ fc, fc', [k] => CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k])
|
||||
, MagicCRef typesNS "plus" 2
|
||||
, MagicCRef (NS typesNS (UN "plus")) 2
|
||||
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n])
|
||||
, MagicCRef typesNS "mult" 2
|
||||
, MagicCRef (NS typesNS (UN "mult")) 2
|
||||
(\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n])
|
||||
, MagicCRef natNS "minus" 2 natMinus
|
||||
, MagicCRef (NS natNS (UN "minus")) 2 natMinus
|
||||
]
|
||||
|
||||
-- get all transformation from %builtin pragmas
|
||||
builtinMagic : Ref Ctxt Defs => Core (forall vars. CExp vars -> CExp vars)
|
||||
builtinMagic = do
|
||||
defs <- get Ctxt
|
||||
let b = defs.builtinTransforms
|
||||
let nats = concatMap builtinMagicNat $ values $ natTyNames b
|
||||
pure $ magic $ natHack ++ nats
|
||||
where
|
||||
builtinMagicNat : NatBuiltin -> List Magic
|
||||
builtinMagicNat cons =
|
||||
[ MagicCCon cons.zero 0
|
||||
(\ fc, [] => CPrimVal fc (BI 0))
|
||||
, MagicCCon cons.succ 1
|
||||
(\ fc, [k] => CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k])
|
||||
] -- TODO: add builtin pragmas for Nat related functions (to/from Integer, add, mult, minus, compare)
|
||||
|
||||
isNatCon : Name -> Bool
|
||||
isNatCon (NS ns (UN n))
|
||||
= (n == "Z" || n == "S") && ns == typesNS
|
||||
isNatCon _ = False
|
||||
isNatCon : (zeroMap : NameMap ZERO) ->
|
||||
(succMap : NameMap SUCC) ->
|
||||
Name -> Bool
|
||||
isNatCon zs ss n = isJust (lookup n zs) || isJust (lookup n ss)
|
||||
|
||||
natBranch : CConAlt vars -> Bool
|
||||
natBranch (MkConAlt n _ _ _) = isNatCon n
|
||||
natBranch : (zeroMap : NameMap ZERO) ->
|
||||
(succMap : NameMap SUCC) ->
|
||||
CConAlt vars -> Bool
|
||||
natBranch zs ss (MkConAlt n _ _ _) = isNatCon zs ss n
|
||||
|
||||
trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
|
||||
trySBranch n (MkConAlt (NS ns (UN nm)) _ [arg] sc)
|
||||
= do guard (nm == "S" && ns == typesNS)
|
||||
trySBranch :
|
||||
(succMap : NameMap SUCC) ->
|
||||
CExp vars ->
|
||||
CConAlt vars ->
|
||||
Maybe (CExp vars)
|
||||
trySBranch ss n (MkConAlt nm _ [arg] sc)
|
||||
= do guard $ isJust $ lookup nm ss
|
||||
let fc = getFC n
|
||||
pure (CLet fc arg True (natMinus fc fc [n, CPrimVal fc (BI 1)]) sc)
|
||||
trySBranch _ _ = Nothing
|
||||
trySBranch _ _ _ = Nothing
|
||||
|
||||
tryZBranch : CConAlt vars -> Maybe (CExp vars)
|
||||
tryZBranch (MkConAlt (NS ns (UN n)) _ [] sc)
|
||||
= do guard (n == "Z" && ns == typesNS)
|
||||
tryZBranch :
|
||||
(zeroMap : NameMap ZERO) ->
|
||||
CConAlt vars ->
|
||||
Maybe (CExp vars)
|
||||
tryZBranch zs (MkConAlt n _ [] sc)
|
||||
= do guard $ isJust $ lookup n zs
|
||||
pure sc
|
||||
tryZBranch _ = Nothing
|
||||
tryZBranch _ _ = Nothing
|
||||
|
||||
getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
|
||||
getSBranch n [] = Nothing
|
||||
getSBranch n (x :: xs) = trySBranch n x <+> getSBranch n xs
|
||||
getSBranch :
|
||||
(succMap : NameMap SUCC) ->
|
||||
CExp vars ->
|
||||
List (CConAlt vars) ->
|
||||
Maybe (CExp vars)
|
||||
getSBranch ss n [] = Nothing
|
||||
getSBranch ss n (x :: xs) = trySBranch ss n x <+> getSBranch ss n xs
|
||||
|
||||
getZBranch : List (CConAlt vars) -> Maybe (CExp vars)
|
||||
getZBranch [] = Nothing
|
||||
getZBranch (x :: xs) = tryZBranch x <+> getZBranch xs
|
||||
getZBranch :
|
||||
(zeroMap : NameMap ZERO) ->
|
||||
List (CConAlt vars) ->
|
||||
Maybe (CExp vars)
|
||||
getZBranch zs [] = Nothing
|
||||
getZBranch zs (x :: xs) = tryZBranch zs x <+> getZBranch zs xs
|
||||
|
||||
-- Rewrite case trees on Nat to be case trees on Integer
|
||||
natHackTree : CExp vars -> CExp vars
|
||||
natHackTree (CConCase fc sc alts def)
|
||||
= if any natBranch alts
|
||||
builtinNatTree' : (zeroMap : NameMap ZERO) ->
|
||||
(succMap : NameMap SUCC) ->
|
||||
CExp vars -> CExp vars
|
||||
builtinNatTree' zs ss (CConCase fc sc alts def)
|
||||
= if any (natBranch zs ss) alts
|
||||
then let defb = maybe (CCrash fc "Nat case not covered") id def
|
||||
scase = maybe defb id (getSBranch sc alts)
|
||||
zcase = maybe defb id (getZBranch alts) in
|
||||
scase = maybe defb id (getSBranch ss sc alts)
|
||||
zcase = maybe defb id (getZBranch zs alts) in
|
||||
CConstCase fc sc [MkConstAlt (BI 0) zcase] (Just scase)
|
||||
else CConCase fc sc alts def
|
||||
natHackTree t = t
|
||||
builtinNatTree' zs ss t = t
|
||||
|
||||
builtinNatTree : Ref Ctxt Defs => Core (CExp vars -> CExp vars)
|
||||
builtinNatTree = do
|
||||
defs <- get Ctxt
|
||||
let b = defs.builtinTransforms
|
||||
pure $ builtinNatTree' b.natZNames b.natSNames
|
||||
|
||||
-- Rewrite case trees on Bool/Ord to be case trees on Integer
|
||||
-- TODO: Generalise to all finite enumerations
|
||||
@ -248,71 +284,75 @@ boolHackTree t = t
|
||||
mutual
|
||||
toCExpTm : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
Name -> Term vars -> Core (CExp vars)
|
||||
toCExpTm n (Local fc _ _ prf)
|
||||
(magic : forall vars. CExp vars -> CExp vars) ->
|
||||
Name -> Term vars ->
|
||||
Core (CExp vars)
|
||||
toCExpTm m n (Local fc _ _ prf)
|
||||
= pure $ CLocal fc prf
|
||||
-- TMP HACK: extend this to all types which look like enumerations after erasure
|
||||
toCExpTm n (Ref fc (DataCon tag arity) fn)
|
||||
toCExpTm m n (Ref fc (DataCon tag arity) fn)
|
||||
= if arity == Z && isFiniteEnum fn
|
||||
then pure $ CPrimVal fc (I tag)
|
||||
else -- get full name for readability, and the Nat hack
|
||||
else -- get full name for readability, and %builtin Natural
|
||||
pure $ CCon fc !(getFullName fn) (Just tag) []
|
||||
toCExpTm n (Ref fc (TyCon tag arity) fn)
|
||||
toCExpTm m n (Ref fc (TyCon tag arity) fn)
|
||||
= pure $ CCon fc fn Nothing []
|
||||
toCExpTm n (Ref fc _ fn)
|
||||
toCExpTm m n (Ref fc _ fn)
|
||||
= do full <- getFullName fn
|
||||
-- ^ For readability of output code, and the Nat hack,
|
||||
pure $ CApp fc (CRef fc full) []
|
||||
toCExpTm n (Meta fc mn i args)
|
||||
= pure $ CApp fc (CRef fc mn) !(traverse (toCExp n) args)
|
||||
toCExpTm n (Bind fc x (Lam _ _ _ _) sc)
|
||||
= pure $ CLam fc x !(toCExp n sc)
|
||||
toCExpTm n (Bind fc x (Let _ rig val _) sc)
|
||||
= do sc' <- toCExp n sc
|
||||
toCExpTm m n (Meta fc mn i args)
|
||||
= pure $ CApp fc (CRef fc mn) !(traverse (toCExp m n) args)
|
||||
toCExpTm m n (Bind fc x (Lam _ _ _ _) sc)
|
||||
= pure $ CLam fc x !(toCExp m n sc)
|
||||
toCExpTm m n (Bind fc x (Let _ rig val _) sc)
|
||||
= do sc' <- toCExp m n sc
|
||||
pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
|
||||
(CLet fc x True !(toCExp n val) sc')
|
||||
(CLet fc x True !(toCExp m n val) sc')
|
||||
rig
|
||||
toCExpTm n (Bind fc x (Pi _ c e ty) sc)
|
||||
= pure $ CCon fc (UN "->") Nothing [!(toCExp n ty),
|
||||
CLam fc x !(toCExp n sc)]
|
||||
toCExpTm n (Bind fc x b tm) = pure $ CErased fc
|
||||
toCExpTm m n (Bind fc x (Pi _ c e ty) sc)
|
||||
= pure $ CCon fc (UN "->") Nothing [!(toCExp m n ty),
|
||||
CLam fc x !(toCExp m n sc)]
|
||||
toCExpTm m n (Bind fc x b tm) = pure $ CErased fc
|
||||
-- We'd expect this to have been dealt with in toCExp, but for completeness...
|
||||
toCExpTm n (App fc tm arg)
|
||||
= pure $ CApp fc !(toCExp n tm) [!(toCExp n arg)]
|
||||
toCExpTm m n (App fc tm arg)
|
||||
= pure $ CApp fc !(toCExp m n tm) [!(toCExp m n arg)]
|
||||
-- This shouldn't be in terms any more, but here for completeness
|
||||
toCExpTm n (As _ _ _ p) = toCExpTm n p
|
||||
toCExpTm m n (As _ _ _ p) = toCExpTm m n p
|
||||
-- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
|
||||
toCExpTm n (TDelayed fc _ _) = pure $ CErased fc
|
||||
toCExpTm n (TDelay fc lr _ arg)
|
||||
= pure (CDelay fc lr !(toCExp n arg))
|
||||
toCExpTm n (TForce fc lr arg)
|
||||
= pure (CForce fc lr !(toCExp n arg))
|
||||
toCExpTm n (PrimVal fc c)
|
||||
toCExpTm m n (TDelayed fc _ _) = pure $ CErased fc
|
||||
toCExpTm m n (TDelay fc lr _ arg)
|
||||
= pure (CDelay fc lr !(toCExp m n arg))
|
||||
toCExpTm m n (TForce fc lr arg)
|
||||
= pure (CForce fc lr !(toCExp m n arg))
|
||||
toCExpTm m n (PrimVal fc c)
|
||||
= let t = constTag c in
|
||||
if t == 0
|
||||
then pure $ CPrimVal fc c
|
||||
else pure $ CCon fc (UN (show c)) Nothing []
|
||||
toCExpTm n (Erased fc _) = pure $ CErased fc
|
||||
toCExpTm n (TType fc) = pure $ CCon fc (UN "Type") Nothing []
|
||||
toCExpTm m n (Erased fc _) = pure $ CErased fc
|
||||
toCExpTm m n (TType fc) = pure $ CCon fc (UN "Type") Nothing []
|
||||
|
||||
toCExp : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
Name -> Term vars -> Core (CExp vars)
|
||||
toCExp n tm
|
||||
(magic : forall vars. CExp vars -> CExp vars) ->
|
||||
Name -> Term vars ->
|
||||
Core (CExp vars)
|
||||
toCExp m n tm
|
||||
= case getFnArgs tm of
|
||||
(f, args) =>
|
||||
do args' <- traverse (toCExp n) args
|
||||
do args' <- traverse (toCExp m n) args
|
||||
defs <- get Ctxt
|
||||
f' <- toCExpTm n f
|
||||
f' <- toCExpTm m n f
|
||||
Arity a <- numArgs defs f
|
||||
| NewTypeBy arity pos =>
|
||||
do let res = applyNewType arity pos f' args'
|
||||
pure $ natHack res
|
||||
pure $ m res
|
||||
| EraseArgs arity epos =>
|
||||
do let res = eraseConArgs arity epos f' args'
|
||||
pure $ natHack res
|
||||
pure $ m res
|
||||
let res = expandToArity a f' args'
|
||||
pure $ natHack res
|
||||
pure $ m res
|
||||
|
||||
mutual
|
||||
conCases : {vars : _} ->
|
||||
@ -448,7 +488,7 @@ mutual
|
||||
def <- getDef n alts
|
||||
if isNil cases
|
||||
then pure (fromMaybe (CErased fc) def)
|
||||
else pure $ boolHackTree $ natHackTree $
|
||||
else pure $ boolHackTree $ !builtinNatTree $
|
||||
CConCase fc (CLocal fc x) cases def
|
||||
toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
|
||||
= throw (InternalError "Unexpected DelayCase")
|
||||
@ -463,7 +503,7 @@ mutual
|
||||
= toCExpTree n sc
|
||||
toCExpTree' n (Case _ x scTy [])
|
||||
= pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
|
||||
toCExpTree' n (STerm _ tm) = toCExp n tm
|
||||
toCExpTree' n (STerm _ tm) = toCExp !builtinMagic n tm
|
||||
toCExpTree' n (Unmatched msg)
|
||||
= pure $ CCrash emptyFC msg
|
||||
toCExpTree' n Impossible
|
||||
@ -658,7 +698,8 @@ export
|
||||
compileExp : {auto c : Ref Ctxt Defs} ->
|
||||
ClosedTerm -> Core (CExp [])
|
||||
compileExp tm
|
||||
= do exp <- toCExp (UN "main") tm
|
||||
= do m <- builtinMagic
|
||||
exp <- toCExp m (UN "main") tm
|
||||
pure exp
|
||||
|
||||
||| Given a name, look up an expression, and compile it to a CExp in the environment
|
||||
|
||||
@ -645,6 +645,61 @@ data Transform : Type where
|
||||
Name -> -- name for identifying the rule
|
||||
Env Term vars -> Term vars -> Term vars -> Transform
|
||||
|
||||
||| Types that are transformed into a faster representation
|
||||
||| during codegen.
|
||||
public export
|
||||
data BuiltinType : Type where
|
||||
||| A built-in 'Nat'-like type
|
||||
||| 'NatLike : [index ->] Type'
|
||||
||| 'SLike : {0 _ : index} -> NatLike [index] -> NatLike [f index]'
|
||||
||| 'ZLike : {0 _ : index} -> NatLike [index]'
|
||||
BuiltinNatural : BuiltinType
|
||||
-- All the following aren't implemented yet
|
||||
-- but are here to reduce number of TTC version changes
|
||||
NaturalPlus : BuiltinType
|
||||
NaturalMult : BuiltinType
|
||||
NaturalToInteger : BuiltinType
|
||||
IntegerToNatural : BuiltinType
|
||||
|
||||
export
|
||||
Show BuiltinType where
|
||||
show BuiltinNatural = "Natural"
|
||||
show _ = "Not yet implemented"
|
||||
|
||||
-- Token types to make it harder to get the constructor names
|
||||
-- the wrong way round.
|
||||
public export data ZERO = MkZERO
|
||||
public export data SUCC = MkSUCC
|
||||
|
||||
||| Record containing names of 'Nat'-like constructors.
|
||||
public export
|
||||
record NatBuiltin where
|
||||
constructor MkNatBuiltin
|
||||
zero : Name
|
||||
succ : Name
|
||||
|
||||
||| Rewrite rules for %builtin pragmas
|
||||
||| Seperate to 'Transform' because it must also modify case statements
|
||||
||| behaviour should remain the same after this transform
|
||||
public export
|
||||
record BuiltinTransforms where
|
||||
constructor MkBuiltinTransforms
|
||||
natTyNames : NameMap NatBuiltin -- map from Nat-like names to their constructors
|
||||
natZNames : NameMap ZERO -- map from Z-like names to their type constructor
|
||||
natSNames : NameMap SUCC -- map from S-like names to their type constructor
|
||||
|
||||
-- TODO: After next release remove nat from here and use %builtin pragma instead
|
||||
initBuiltinTransforms : BuiltinTransforms
|
||||
initBuiltinTransforms =
|
||||
let type = NS typesNS (UN "Nat")
|
||||
zero = NS typesNS (UN "Z")
|
||||
succ = NS typesNS (UN "S")
|
||||
in MkBuiltinTransforms
|
||||
{ natTyNames = singleton type (MkNatBuiltin {zero, succ})
|
||||
, natZNames = singleton zero MkZERO
|
||||
, natSNames = singleton succ MkSUCC
|
||||
}
|
||||
|
||||
export
|
||||
getFnName : Transform -> Maybe Name
|
||||
getFnName (MkTransform _ _ app _)
|
||||
@ -987,6 +1042,10 @@ record Defs where
|
||||
-- ^ A mapping from names to transformation rules which update applications
|
||||
-- of that name
|
||||
saveTransforms : List (Name, Transform)
|
||||
builtinTransforms : BuiltinTransforms
|
||||
-- ^ A mapping from names to transformations resulting from a %builtin pragma
|
||||
-- seperate to `transforms` because these must always fire globally so run these
|
||||
-- when compiling to `CExp`.
|
||||
namedirectives : NameMap (List String)
|
||||
ifaceHash : Int
|
||||
importHashes : List (Namespace, Int)
|
||||
@ -1046,6 +1105,7 @@ initDefs
|
||||
, saveAutoHints = []
|
||||
, transforms = empty
|
||||
, saveTransforms = []
|
||||
, builtinTransforms = initBuiltinTransforms
|
||||
, namedirectives = empty
|
||||
, ifaceHash = 5381
|
||||
, importHashes = []
|
||||
|
||||
@ -991,6 +991,7 @@ mutual
|
||||
Overloadable n => pure [IPragma [] (\nest, env => setNameFlag fc n Overloadable)]
|
||||
Extension e => pure [IPragma [] (\nest, env => setExtension e)]
|
||||
DefaultTotality tot => pure [IPragma [] (\_, _ => setDefaultTotalityOption tot)]
|
||||
desugarDecl ps (PBuiltin fc type name) = pure [IBuiltin fc type name]
|
||||
|
||||
export
|
||||
desugar : {auto s : Ref Syn SyntaxInfo} ->
|
||||
|
||||
@ -1199,6 +1199,20 @@ fnDirectOpt fname
|
||||
cs <- block (expr pdef fname)
|
||||
pure $ PForeign cs
|
||||
|
||||
builtinType : Rule BuiltinType
|
||||
builtinType =
|
||||
BuiltinNatural <$ exactIdent "Natural"
|
||||
|
||||
builtinDecl : FileName -> IndentInfo -> Rule PDecl
|
||||
builtinDecl fname indents
|
||||
= do b <- bounds (do pragma "builtin"
|
||||
commit
|
||||
t <- builtinType
|
||||
n <- name
|
||||
pure (t, n))
|
||||
(t, n) <- pure b.val
|
||||
pure $ PBuiltin (boundToFC fname b) t n
|
||||
|
||||
visOpt : FileName -> Rule (Either Visibility PFnOpt)
|
||||
visOpt fname
|
||||
= do vis <- visOption
|
||||
@ -1430,6 +1444,8 @@ topDecl fname indents
|
||||
pure [d]
|
||||
<|> do d <- usingDecls fname indents
|
||||
pure [d]
|
||||
<|> do d <- builtinDecl fname indents
|
||||
pure [d]
|
||||
<|> do d <- runElabDecl fname indents
|
||||
pure [d]
|
||||
<|> do d <- transformDecl fname indents
|
||||
|
||||
@ -440,6 +440,7 @@ mutual
|
||||
= pure (Just (PRunElabDecl fc !(toPTerm startPrec tm)))
|
||||
toPDecl (IPragma _ _) = pure Nothing
|
||||
toPDecl (ILog _) = pure Nothing
|
||||
toPDecl (IBuiltin fc type name) = pure $ Just $ PBuiltin fc type name
|
||||
|
||||
export
|
||||
cleanPTerm : {auto c : Ref Ctxt Defs} ->
|
||||
|
||||
@ -337,6 +337,7 @@ mutual
|
||||
PTransform : FC -> String -> PTerm -> PTerm -> PDecl
|
||||
PRunElabDecl : FC -> PTerm -> PDecl
|
||||
PDirective : FC -> Directive -> PDecl
|
||||
PBuiltin : FC -> BuiltinType -> Name -> PDecl
|
||||
|
||||
export
|
||||
getPDeclLoc : PDecl -> FC
|
||||
@ -355,6 +356,7 @@ mutual
|
||||
getPDeclLoc (PTransform fc _ _ _) = fc
|
||||
getPDeclLoc (PRunElabDecl fc _) = fc
|
||||
getPDeclLoc (PDirective fc _) = fc
|
||||
getPDeclLoc (PBuiltin fc _ _) = fc
|
||||
|
||||
export
|
||||
isPDef : PDecl -> Maybe (FC, List PClause)
|
||||
@ -1087,6 +1089,7 @@ mapPTermM f = goPTerm where
|
||||
goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b
|
||||
goPDecl (PRunElabDecl fc a) = PRunElabDecl fc <$> goPTerm a
|
||||
goPDecl p@(PDirective _ _) = pure p
|
||||
goPDecl p@(PBuiltin _ _ _) = pure p
|
||||
|
||||
|
||||
goPTypeDecl : PTypeDecl -> Core PTypeDecl
|
||||
|
||||
@ -223,6 +223,10 @@ export
|
||||
empty : NameMap v
|
||||
empty = Empty
|
||||
|
||||
export
|
||||
singleton : Name -> v -> NameMap v
|
||||
singleton n v = M Z $ Leaf n v
|
||||
|
||||
export
|
||||
lookup : Name -> NameMap v -> Maybe v
|
||||
lookup _ Empty = Nothing
|
||||
|
||||
@ -662,6 +662,10 @@ logLevel
|
||||
lvl <- intLit
|
||||
pure (Just (topic, fromInteger lvl))
|
||||
|
||||
builtinType : Rule BuiltinType
|
||||
builtinType =
|
||||
BuiltinNatural <$ exactIdent "Natural"
|
||||
|
||||
directive : FileName -> IndentInfo -> Rule ImpDecl
|
||||
directive fname indents
|
||||
= do pragma "logging"
|
||||
@ -669,6 +673,14 @@ directive fname indents
|
||||
lvl <- logLevel
|
||||
atEnd indents
|
||||
pure (ILog lvl)
|
||||
<|> do b <- bounds (do pragma "builtin"
|
||||
commit
|
||||
t <- builtinType
|
||||
n <- name
|
||||
pure (t, n))
|
||||
(t, n) <- pure b.val
|
||||
pure $ IBuiltin (boundToFC fname b) t n
|
||||
|
||||
{- Can't do IPragma due to lack of Ref Ctxt. Should we worry about this?
|
||||
<|> do pragma "pair"
|
||||
commit
|
||||
|
||||
173
src/TTImp/ProcessBuiltin.idr
Normal file
173
src/TTImp/ProcessBuiltin.idr
Normal file
@ -0,0 +1,173 @@
|
||||
||| Checking a %builtin pragma is correct.
|
||||
-- If we get more builtins it might be wise to move each builtin to it's own file.
|
||||
module TTImp.ProcessBuiltin
|
||||
|
||||
import Libraries.Data.Bool.Extra
|
||||
import Libraries.Data.NameMap
|
||||
import Data.List
|
||||
|
||||
import Core.Core
|
||||
import Core.Context
|
||||
import Core.Context.Log
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.TT
|
||||
import Core.UnifyState
|
||||
|
||||
import TTImp.TTImp
|
||||
|
||||
||| Get the return type.
|
||||
getRetTy : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
|
||||
getRetTy tm@(Bind _ x b scope) = case b of
|
||||
Lam _ _ _ _ => Nothing
|
||||
Let _ _ val _ => getRetTy $ subst {x} val scope
|
||||
Pi _ _ _ _ => getRetTy scope
|
||||
_ => Nothing
|
||||
getRetTy tm = Just (vars ** tm)
|
||||
|
||||
||| Get the first non-erased argument type.
|
||||
getFirstNETy : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
|
||||
getFirstNETy (Bind _ x b tm) = case b of
|
||||
Let _ _ val _ => getFirstNETy $ subst {x} val tm
|
||||
Pi _ mul _ arg => if isErased mul
|
||||
then getFirstNETy tm
|
||||
else Just (_ ** arg)
|
||||
_ => Nothing
|
||||
getFirstNETy tm = Nothing
|
||||
|
||||
||| Do the terms match ignoring arguments to type constructors.
|
||||
termConMatch : Term vs -> Term vs' -> Bool
|
||||
termConMatch (Local _ _ x _) (Local _ _ y _) = x == y
|
||||
termConMatch (Ref _ _ n) (Ref _ _ m) = n == m
|
||||
termConMatch (Meta _ _ i args0) (Meta _ _ j args1)
|
||||
= i == j && allTrue (zipWith termConMatch args0 args1)
|
||||
-- I don't understand how they're equal if args are different lengths
|
||||
-- but this is what's in Core.TT.
|
||||
termConMatch (Bind _ _ b s) (Bind _ _ c t) = eqBinderBy termConMatch b c && termConMatch s t
|
||||
termConMatch (App _ f _) (App _ g _) = termConMatch f g
|
||||
termConMatch (As _ _ a p) (As _ _ b q) = termConMatch a b && termConMatch p q
|
||||
termConMatch (TDelayed _ _ tm0) tm1 = termConMatch tm0 tm1
|
||||
termConMatch tm0 (TDelayed _ _ tm1) = termConMatch tm0 tm1
|
||||
-- don't check for laziness here to give more accurate error messages.
|
||||
termConMatch (TDelay _ _ tm0 x0) (TDelay _ _ tm1 x1) = termConMatch tm0 tm1 && termConMatch x0 x1
|
||||
termConMatch (TForce _ _ tm0) tm1 = termConMatch tm0 tm1
|
||||
termConMatch tm0 (TForce _ _ tm1) = termConMatch tm0 tm1
|
||||
termConMatch (PrimVal _ _) (PrimVal _ _) = True -- no constructor to check.
|
||||
termConMatch (Erased _ _) (Erased _ _) = True -- return type can't erased?
|
||||
termConMatch (TType _) (TType _) = True
|
||||
termConMatch _ _ = False
|
||||
|
||||
||| Check a type is strict.
|
||||
isStrict : Term vs -> Bool
|
||||
isStrict (Local _ _ _ _) = True
|
||||
isStrict (Ref _ _ _) = True
|
||||
isStrict (Meta _ _ i args) = all isStrict args
|
||||
isStrict (Bind _ _ b s) = isStrict (binderType b) && isStrict s
|
||||
isStrict (App _ f x) = isStrict f && isStrict x
|
||||
isStrict (As _ _ a p) = isStrict a && isStrict p
|
||||
isStrict (TDelayed _ _ _) = False
|
||||
isStrict (TDelay _ _ f x) = isStrict f && isStrict x
|
||||
isStrict (TForce _ _ tm) = isStrict tm
|
||||
isStrict (PrimVal _ _) = True
|
||||
isStrict (Erased _ _) = True
|
||||
isStrict (TType _) = True
|
||||
|
||||
||| Get the name and arity (of non-erased arguments only) of a list of names.
|
||||
||| `cons` should all be data constructors (`DCon`) otherwise it will throw an error.
|
||||
getConsGDef : Context -> FC -> (cons : List Name) -> Core $ List (Name, GlobalDef)
|
||||
getConsGDef c fc = traverse \n => do
|
||||
[(n', _, gdef)] <- lookupCtxtName n c
|
||||
| [] => throw $ UndefinedName fc n
|
||||
| ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
|
||||
pure (n', gdef)
|
||||
|
||||
||| Check a list of constructors has exactly
|
||||
||| 1 'Z'-like constructor
|
||||
||| and 1 `S`-like constructor, which has type `ty -> ty` or `ty arg -> `ty (f arg)`.
|
||||
checkCons : Context -> (cons : List (Name, GlobalDef)) -> (dataType : Name) -> FC -> Core NatBuiltin
|
||||
checkCons c cons ty fc = case !(foldr checkCon (pure (Nothing, Nothing)) cons) of
|
||||
(Just zero, Just succ) => pure $ MkNatBuiltin {zero, succ}
|
||||
(Nothing, _) => throw $ GenericMsg fc $ "No 'Z'-like constructors for " ++ show ty ++ "."
|
||||
(_, Nothing) => throw $ GenericMsg fc $ "No 'S'-like constructors for " ++ show ty ++ "."
|
||||
where
|
||||
||| Check if a list of names contains a name.
|
||||
checkSArgType : List Name -> Core ()
|
||||
checkSArgType [] = throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " is missing argument of type: " ++ show ty
|
||||
checkSArgType (n :: ns) = if nameRoot n == nameRoot ty && (n `matches` ty)
|
||||
then checkSArgType ns
|
||||
else throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " has unexpected argument: " ++ show n
|
||||
|
||||
||| Check the type of an 'S'-like constructor.
|
||||
checkTyS : Name -> GlobalDef -> Core ()
|
||||
checkTyS n gdef = do
|
||||
let type = gdef.type
|
||||
erase = gdef.eraseArgs
|
||||
let Just (_ ** arg) = getFirstNETy type
|
||||
| Nothing => throw $ InternalError "Expected a non-erased argument, found none."
|
||||
let Just (_ ** ret) = getRetTy type
|
||||
| Nothing => throw $ InternalError $ "Unexpected type " ++ show type
|
||||
unless (termConMatch arg ret) $ throw $ GenericMsg fc $ "Incorrect type for 'S'-like constructor for " ++ show ty ++ "."
|
||||
unless (isStrict arg) $ throw $ GenericMsg fc $ "Natural builtin does not support lazy types, as they can be potentially infinite."
|
||||
pure ()
|
||||
|
||||
||| Check a constructor's arity and type.
|
||||
-- 'Z'-like constructor is always first, then 'S'-like constructor.
|
||||
checkCon : (Name, GlobalDef) -> Core (Maybe Name, Maybe Name) -> Core (Maybe Name, Maybe Name)
|
||||
checkCon (n, gdef) cons = do
|
||||
(zero, succ) <- cons
|
||||
let DCon _ arity _ = gdef.definition
|
||||
| def => throw $ GenericMsg fc $ "Expected data constructor, found:\n" ++ show def
|
||||
case arity `minus` length gdef.eraseArgs of
|
||||
0 => case zero of
|
||||
Just _ => throw $ GenericMsg fc $ "Multiple 'Z'-like constructors for " ++ show ty ++ "."
|
||||
Nothing => pure (Just n, succ)
|
||||
1 => case succ of
|
||||
Just _ => throw $ GenericMsg fc $ "Multiple 'S'-like constructors for " ++ show ty ++ "."
|
||||
Nothing => do
|
||||
checkTyS n gdef
|
||||
pure (zero, Just n)
|
||||
_ => throw $ GenericMsg fc $ "Constructor " ++ show n ++ " doesn't match any pattern for Natural."
|
||||
|
||||
addBuiltinNat :
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
(ty : Name) -> NatBuiltin -> Core ()
|
||||
addBuiltinNat type cons = do
|
||||
log "builtin.Natural.addTransform" 10 $ "Add Builtin Natural transform for " ++ show type
|
||||
update Ctxt $ record
|
||||
{ builtinTransforms.natTyNames $= insert type cons
|
||||
, builtinTransforms.natZNames $= insert cons.zero MkZERO
|
||||
, builtinTransforms.natSNames $= insert cons.succ MkSUCC
|
||||
}
|
||||
|
||||
||| Check a `%builtin Natural` pragma is correct.
|
||||
processBuiltinNatural :
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Defs -> FC -> Name -> Core ()
|
||||
processBuiltinNatural ds fc name = do
|
||||
log "builtin.Natural" 5 $ "Processing Builtin Natural pragma for " ++ show name
|
||||
[(n, _, gdef)] <- lookupCtxtName name ds.gamma
|
||||
| [] => throw $ UndefinedName fc name
|
||||
| ns => throw $ AmbiguousName fc $ (\(n, _, _) => n) <$> ns
|
||||
let TCon _ _ _ _ _ _ dcons _ = gdef.definition
|
||||
| def => throw $ GenericMsg fc $ "Expected a type constructor, found:\n" ++ show def
|
||||
cons <- getConsGDef ds.gamma fc dcons
|
||||
cons <- checkCons ds.gamma cons n fc
|
||||
zero <- getFullName cons.zero
|
||||
succ <- getFullName cons.succ
|
||||
n <- getFullName name
|
||||
addBuiltinNat n $ MkNatBuiltin {zero, succ}
|
||||
|
||||
||| Check a `%builtin` pragma is correct.
|
||||
export
|
||||
processBuiltin :
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
NestedNames vars -> Env Term vars -> FC -> BuiltinType -> Name -> Core ()
|
||||
processBuiltin nest env fc type name = do
|
||||
ds <- get Ctxt
|
||||
case type of
|
||||
BuiltinNatural => processBuiltinNatural ds fc name
|
||||
_ => throw $ InternalError $ "%builtin " ++ show type ++ " not yet implemented."
|
||||
@ -13,6 +13,7 @@ import Parser.Source
|
||||
import TTImp.BindImplicits
|
||||
import TTImp.Elab.Check
|
||||
import TTImp.Parser
|
||||
import TTImp.ProcessBuiltin
|
||||
import TTImp.ProcessData
|
||||
import TTImp.ProcessDef
|
||||
import TTImp.ProcessParams
|
||||
@ -60,6 +61,8 @@ process eopts nest env (IPragma _ act)
|
||||
= act nest env
|
||||
process eopts nest env (ILog lvl)
|
||||
= addLogLevel (uncurry unsafeMkLogLevel <$> lvl)
|
||||
process eopts nest env (IBuiltin fc type name)
|
||||
= processBuiltin nest env fc type name
|
||||
|
||||
TTImp.Elab.Check.processDecl = process
|
||||
|
||||
|
||||
@ -765,3 +765,5 @@ mutual
|
||||
reflect fc defs lhs env (ILog x)
|
||||
= do x' <- reflect fc defs lhs env x
|
||||
appCon fc defs (reflectionttimp "ILog") [x']
|
||||
reflect fc defs lhs env (IBuiltin _ _ _)
|
||||
= throw (GenericMsg fc "Can't reflect a %builtin")
|
||||
|
||||
@ -356,6 +356,7 @@ mutual
|
||||
NestedNames vars -> Env Term vars -> Core ()) ->
|
||||
ImpDecl
|
||||
ILog : Maybe (List String, Nat) -> ImpDecl
|
||||
IBuiltin : FC -> BuiltinType -> Name -> ImpDecl
|
||||
|
||||
export
|
||||
Show ImpDecl where
|
||||
@ -378,6 +379,7 @@ mutual
|
||||
show (ILog (Just (topic, lvl))) = "%logging " ++ case topic of
|
||||
[] => show lvl
|
||||
_ => concat (intersperse "." topic) ++ " " ++ show lvl
|
||||
show (IBuiltin _ type name) = "%builtin " ++ show type ++ " " ++ show name
|
||||
|
||||
export
|
||||
isIPrimVal : RawImp -> Maybe Constant
|
||||
@ -740,6 +742,22 @@ getFn f = f
|
||||
|
||||
-- Everything below is TTC instances
|
||||
|
||||
export
|
||||
TTC BuiltinType where
|
||||
toBuf b BuiltinNatural = tag 0
|
||||
toBuf b NaturalPlus = tag 1
|
||||
toBuf b NaturalMult = tag 2
|
||||
toBuf b NaturalToInteger = tag 3
|
||||
toBuf b IntegerToNatural = tag 4
|
||||
|
||||
fromBuf b = case !getTag of
|
||||
0 => pure BuiltinNatural
|
||||
1 => pure NaturalPlus
|
||||
2 => pure NaturalMult
|
||||
3 => pure NaturalToInteger
|
||||
4 => pure IntegerToNatural
|
||||
_ => corrupt "BuiltinType"
|
||||
|
||||
mutual
|
||||
export
|
||||
TTC RawImp where
|
||||
@ -1103,6 +1121,8 @@ mutual
|
||||
toBuf b (IPragma _ f) = throw (InternalError "Can't write Pragma")
|
||||
toBuf b (ILog n)
|
||||
= do tag 8; toBuf b n
|
||||
toBuf b (IBuiltin fc type name)
|
||||
= do tag 9; toBuf b fc; toBuf b type; toBuf b name
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
@ -1132,6 +1152,10 @@ mutual
|
||||
pure (IRunElabDecl fc tm)
|
||||
8 => do n <- fromBuf b
|
||||
pure (ILog n)
|
||||
9 => do fc <- fromBuf b
|
||||
type <- fromBuf b
|
||||
name <- fromBuf b
|
||||
pure (IBuiltin fc type name)
|
||||
_ => corrupt "ImpDecl"
|
||||
|
||||
|
||||
|
||||
@ -136,6 +136,11 @@ idrisTestsData = MkTestPool []
|
||||
"record001", "record002", "record003", "record004", "record005",
|
||||
"record006", "record007"]
|
||||
|
||||
idrisTestsBuiltin : TestPool
|
||||
idrisTestsBuiltin = MkTestPool []
|
||||
-- %builtin related tests for the frontend (type-checking)
|
||||
["builtin001", "builtin002", "builtin003", "builtin004"]
|
||||
|
||||
idrisTestsEvaluator : TestPool
|
||||
idrisTestsEvaluator = MkTestPool []
|
||||
[ -- Evaluator
|
||||
@ -269,6 +274,7 @@ contribLibraryTests = MkTestPool [Chez, Node]
|
||||
codegenTests : TestPool
|
||||
codegenTests = MkTestPool []
|
||||
[ "con001"
|
||||
, "builtin001"
|
||||
]
|
||||
|
||||
main : IO ()
|
||||
@ -285,6 +291,7 @@ main = runner
|
||||
, testPaths "idris2" idrisTestsPerformance
|
||||
, testPaths "idris2" idrisTestsRegression
|
||||
, testPaths "idris2" idrisTestsData
|
||||
, testPaths "idris2" idrisTestsBuiltin
|
||||
, testPaths "idris2" idrisTestsEvaluator
|
||||
, testPaths "idris2" idrisTests
|
||||
, testPaths "typedd-book" typeddTests
|
||||
|
||||
7
tests/codegen/builtin001/CatCases.idr
Normal file
7
tests/codegen/builtin001/CatCases.idr
Normal file
@ -0,0 +1,7 @@
|
||||
import System.File
|
||||
|
||||
main : IO ()
|
||||
main = do
|
||||
Right str <- readFile "Main.cases"
|
||||
| Left err => putStrLn "Error:" *> printLn err
|
||||
putStrLn str
|
||||
13
tests/codegen/builtin001/Main.idr
Normal file
13
tests/codegen/builtin001/Main.idr
Normal file
@ -0,0 +1,13 @@
|
||||
|
||||
data Natural : Type where
|
||||
S : Natural -> Natural
|
||||
Z : Natural
|
||||
|
||||
%builtin Natural Natural
|
||||
|
||||
plus : Natural -> Natural -> Natural
|
||||
plus Z y = y
|
||||
plus (S x) y = S (plus x y)
|
||||
|
||||
main : IO Natural
|
||||
main = pure $ plus (S Z) (S $ S Z)
|
||||
36
tests/codegen/builtin001/expected
Normal file
36
tests/codegen/builtin001/expected
Normal file
@ -0,0 +1,36 @@
|
||||
Dumping case trees to Main.cases
|
||||
prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
|
||||
prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
|
||||
prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
|
||||
prim__lte_Integer = [{arg:N}, {arg:N}]: (<=Integer [!{arg:N}, !{arg:N}])
|
||||
prim__believe_me = [{arg:N}, {arg:N}, {arg:N}]: (believe_me [!{arg:N}, !{arg:N}, !{arg:N}])
|
||||
Main.plus = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N})] Just (%let {e:N} (-Integer [!{arg:N}, 1]) (+Integer [1, (Main.plus [!{e:N}, !{arg:N}])])))
|
||||
Main.main = [{ext:N}]: (Main.plus [(+Integer [1, 0]), (+Integer [1, (+Integer [1, 0])])])
|
||||
Main.Z = Constructor tag Just 1 arity 0
|
||||
Main.S = Constructor tag Just 0 arity 1
|
||||
Prelude.Basics.intToBool = [{arg:N}]: (%case !{arg:N} [(%constcase 0 1)] Just 0)
|
||||
Prelude.Basics.True = Constructor tag Just 0 arity 0
|
||||
Prelude.Basics.False = Constructor tag Just 1 arity 0
|
||||
Builtin.believe_me = [{arg:N}, {arg:N}, {ext:N}]: (believe_me [___, ___, !{ext:N}])
|
||||
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [___, ___, !{arg:N}])), (%constcase 1 0)] 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.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)
|
||||
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}])])
|
||||
PrimIO.unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeCreateWorld [___, (%lam w (PrimIO.case block in unsafePerformIO [___, !{arg:N}, ___, (!{arg:N} [!w])]))])
|
||||
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}, {arg:N}]: !{arg:N}
|
||||
PrimIO.unsafeCreateWorld = [{arg:N}, {arg:N}]: (!{arg:N} [%MkWorld])
|
||||
PrimIO.io_pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
|
||||
PrimIO.io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (PrimIO.case block in io_bind [___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{ext:N}])])
|
||||
PrimIO.MkIORes = Constructor tag Just 0 arity 3 (newtype by 1)
|
||||
PrimIO.MkIO = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.IO.pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
|
||||
Prelude.IO.map = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (!{arg:N} [!{act:N}]))
|
||||
Prelude.IO.Functor implementation at Prelude/IO.idr:L:C--L:C = [{ext:N}, {ext:N}, {ext:N}, {ext:N}, {ext:N}]: (Prelude.IO.map [___, ___, !{ext:N}, !{ext:N}, !{ext:N}])
|
||||
Prelude.IO.Applicative implementation at Prelude/IO.idr:L:C--L:C = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam b (%lam a (%lam func (%lam {arg:N} (%lam {eta:N} (Prelude.IO.map [___, ___, !func, !{arg:N}, !{eta:N}])))))), (%lam a (%lam {arg:N} (%lam {eta:N} !{arg:N}))), (%lam b (%lam a (%lam {arg:N} (%lam {arg:N} (%lam {eta:N} (%let {act:N} (!{arg:N} [!{eta:N}]) (%let {act:N} (!{arg:N} [!{eta:N}]) (!{act:N} [!{act:N}]))))))))])
|
||||
Prelude.IO.<*> = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (%let {act:N} (!{arg:N} [!{ext:N}]) (!{act:N} [!{act:N}])))
|
||||
|
||||
6
tests/codegen/builtin001/run
Executable file
6
tests/codegen/builtin001/run
Executable file
@ -0,0 +1,6 @@
|
||||
$1 --no-color --console-width 0 --no-banner --dumpcases Main.cases -o Main Main.idr
|
||||
|
||||
$1 --no-color --console-width 0 --no-banner --exec main CatCases.idr | sed -E "s/[0-9]+}/N}/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g"
|
||||
|
||||
rm -rf build
|
||||
rm Main.cases
|
||||
@ -1,128 +1,128 @@
|
||||
Dumping case trees to Main.cases
|
||||
prim__add_Int = [{arg:0}, {arg:1}]: (+Int [!{arg:0}, !{arg:1}])
|
||||
prim__add_Integer = [{arg:0}, {arg:1}]: (+Integer [!{arg:0}, !{arg:1}])
|
||||
prim__sub_Int = [{arg:0}, {arg:1}]: (-Int [!{arg:0}, !{arg:1}])
|
||||
prim__sub_Integer = [{arg:0}, {arg:1}]: (-Integer [!{arg:0}, !{arg:1}])
|
||||
prim__mul_Int = [{arg:0}, {arg:1}]: (*Int [!{arg:0}, !{arg:1}])
|
||||
prim__mul_Integer = [{arg:0}, {arg:1}]: (*Integer [!{arg:0}, !{arg:1}])
|
||||
prim__div_Int = [{arg:0}, {arg:1}]: (/Int [!{arg:0}, !{arg:1}])
|
||||
prim__mod_Int = [{arg:0}, {arg:1}]: (%Int [!{arg:0}, !{arg:1}])
|
||||
prim__lt_Int = [{arg:0}, {arg:1}]: (<Int [!{arg:0}, !{arg:1}])
|
||||
prim__lte_Int = [{arg:0}, {arg:1}]: (<=Int [!{arg:0}, !{arg:1}])
|
||||
prim__lte_Integer = [{arg:0}, {arg:1}]: (<=Integer [!{arg:0}, !{arg:1}])
|
||||
prim__eq_Int = [{arg:0}, {arg:1}]: (==Int [!{arg:0}, !{arg:1}])
|
||||
prim__gte_Int = [{arg:0}, {arg:1}]: (>=Int [!{arg:0}, !{arg:1}])
|
||||
prim__gt_Int = [{arg:0}, {arg:1}]: (>Int [!{arg:0}, !{arg:1}])
|
||||
prim__believe_me = [{arg:0}, {arg:1}, {arg:2}]: (believe_me [!{arg:0}, !{arg:1}, !{arg:2}])
|
||||
prim__crash = [{arg:0}, {arg:1}]: (crash [!{arg:0}, !{arg:1}])
|
||||
prim__cast_IntegerInt = [{arg:0}]: (cast-Integer-Int [!{arg:0}])
|
||||
Main.main = [{ext:0}]: ((Prelude.Interfaces.sum [___, ___, (%con Builtin.MkPair Just 0 [(%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:227:1--252:55 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:1144} (Prelude.Types.null [___, !{arg:1144}])))]), (%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))])])]) [(Prelude.Types.rangeFromTo [___, (%con Builtin.MkPair Just 0 [(%con Prelude.Num.Integral at Prelude/Num.idr:48:1--53:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:184} (%lam {arg:185} (Prelude.Num.div [!{arg:184}, !{arg:185}]))), (%lam {arg:186} (%lam {arg:187} (Prelude.Num.mod [!{arg:186}, !{arg:187}])))]), (%con Builtin.MkPair Just 0 [(%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [(%lam {arg:2} (%lam {arg:3} (Prelude.EqOrd.== [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (Prelude.EqOrd./= [!{arg:4}, !{arg:5}])))]), (%lam {arg:371} (%lam {arg:372} (Prelude.EqOrd.compare [!{arg:371}, !{arg:372}]))), (%lam {arg:373} (%lam {arg:374} (Prelude.EqOrd.< [!{arg:373}, !{arg:374}]))), (%lam {arg:375} (%lam {arg:376} (Prelude.EqOrd.> [!{arg:375}, !{arg:376}]))), (%lam {arg:377} (%lam {arg:378} (Prelude.EqOrd.<= [!{arg:377}, !{arg:378}]))), (%lam {arg:379} (%lam {arg:380} (Prelude.EqOrd.>= [!{arg:379}, !{arg:380}]))), (%lam {arg:381} (%lam {arg:382} (Prelude.EqOrd.max [!{arg:381}, !{arg:382}]))), (%lam {arg:383} (%lam {arg:384} (Prelude.EqOrd.min [!{arg:383}, !{arg:384}])))]), (%con Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:56} (Prelude.Num.negate [!{arg:56}])), (%lam {arg:57} (%lam {arg:58} (Prelude.Num.- [!{arg:57}, !{arg:58}])))])])]), (cast-Integer-Int [1]), (cast-Integer-Int [100])])])
|
||||
Prelude.Basics.not = [{arg:0}]: (%case !{arg:0} [(%constcase 0 1), (%constcase 1 0)] Nothing)
|
||||
Prelude.Basics.intToBool = [{arg:0}]: (%case !{arg:0} [(%constcase 0 1)] Just 0)
|
||||
prim__add_Int = [{arg:N}, {arg:N}]: (+Int [!{arg:N}, !{arg:N}])
|
||||
prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
|
||||
prim__sub_Int = [{arg:N}, {arg:N}]: (-Int [!{arg:N}, !{arg:N}])
|
||||
prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
|
||||
prim__mul_Int = [{arg:N}, {arg:N}]: (*Int [!{arg:N}, !{arg:N}])
|
||||
prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
|
||||
prim__div_Int = [{arg:N}, {arg:N}]: (/Int [!{arg:N}, !{arg:N}])
|
||||
prim__mod_Int = [{arg:N}, {arg:N}]: (%Int [!{arg:N}, !{arg:N}])
|
||||
prim__lt_Int = [{arg:N}, {arg:N}]: (<Int [!{arg:N}, !{arg:N}])
|
||||
prim__lte_Int = [{arg:N}, {arg:N}]: (<=Int [!{arg:N}, !{arg:N}])
|
||||
prim__lte_Integer = [{arg:N}, {arg:N}]: (<=Integer [!{arg:N}, !{arg:N}])
|
||||
prim__eq_Int = [{arg:N}, {arg:N}]: (==Int [!{arg:N}, !{arg:N}])
|
||||
prim__gte_Int = [{arg:N}, {arg:N}]: (>=Int [!{arg:N}, !{arg:N}])
|
||||
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])])])
|
||||
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
|
||||
Prelude.Basics.False = Constructor tag Just 1 arity 0
|
||||
Prelude.Basics.Bool = Constructor tag Nothing arity 0
|
||||
Prelude.Basics.&& = [{arg:0}, {arg:1}]: (%case !{arg:0} [(%constcase 0 (%force Lazy !{arg:1})), (%constcase 1 1)] Nothing)
|
||||
Builtin.snd = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Builtin.MkPair Just 0 [{e:2}, {e:3}] !{e:3})] Nothing)
|
||||
Builtin.idris_crash = [{arg:0}, {ext:0}]: (crash [___, !{ext:0}])
|
||||
Builtin.fst = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Builtin.MkPair Just 0 [{e:2}, {e:3}] !{e:2})] Nothing)
|
||||
Builtin.believe_me = [{arg:0}, {arg:1}, {ext:0}]: (believe_me [___, ___, !{ext:0}])
|
||||
Builtin.assert_total = [{arg:0}, {arg:1}]: !{arg:1}
|
||||
Prelude.Basics.&& = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%force Lazy !{arg:N})), (%constcase 1 1)] Nothing)
|
||||
Builtin.snd = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
|
||||
Builtin.idris_crash = [{arg:N}, {ext:N}]: (crash [___, !{ext:N}])
|
||||
Builtin.fst = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
|
||||
Builtin.believe_me = [{arg:N}, {arg:N}, {ext:N}]: (believe_me [___, ___, !{ext:N}])
|
||||
Builtin.assert_total = [{arg:N}, {arg:N}]: !{arg:N}
|
||||
Builtin.MkPair = Constructor tag Just 0 arity 2
|
||||
Prelude.Types.case block in rangeFromThen = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:5} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [!{arg:5}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)]))] Nothing))])), (%constcase 1 (Prelude.Types.countFrom [___, !{arg:2}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:3} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:2}]) [!{arg:3}]))] Nothing)]))] Nothing))]))] Nothing)
|
||||
Prelude.Types.case block in case block in case block in rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (%case !{arg:5} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:2}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.Nil Just 0 []))] Nothing)
|
||||
Prelude.Types.case block in case block in rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (%case !{arg:5} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:6} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:3} [!{arg:6}]) [!{arg:2}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:4}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:3} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:4}]) [!{arg:3}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in case block in rangeFromThenTo [___, !{arg:1}, !{arg:4}, !{arg:3}, !{arg:2}, (Prelude.Basics.&& [(%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] !{e:1})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [{e:1}, {e:2}] ((!{e:1} [!{arg:4}]) [!{arg:3}]))] Nothing), (%delay Lazy (%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] !{e:1})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [{e:1}, {e:2}] ((!{e:1} [!{arg:3}]) [!{arg:2}]))] Nothing))])]))] Nothing)
|
||||
Prelude.Types.case block in rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (%case !{arg:5} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:6} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:6}]) [!{arg:4}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:6} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [!{arg:6}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromThenTo [___, !{arg:1}, !{arg:4}, !{arg:3}, !{arg:2}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:3} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:2}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:3}]))] Nothing)]))] Nothing)]))] Nothing)
|
||||
Prelude.Types.case block in case block in rangeFromTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:5} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:5} [!{arg:5}]) [!{arg:2}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:3}, (%lam x (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:3} [!x]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] !{e:6})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:3}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
|
||||
Prelude.Types.case block in rangeFromTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:5} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:6} [!{arg:5}]) [!{arg:3}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:5} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [!{arg:5}]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] !{e:6})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [___, !{arg:1}, !{arg:3}, !{arg:2}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:2}]) [!{arg:3}]))] Nothing)]))] Nothing)
|
||||
Prelude.Types.case block in takeBefore = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (%con Prelude.Types.Nil Just 0 [])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:1}, (Prelude.Types.takeBefore [___, !{arg:3}, (%force Inf !{arg:2})])]))] Nothing)
|
||||
Prelude.Types.case block in takeUntil = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:1}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:1}, (Prelude.Types.takeUntil [___, !{arg:3}, (%force Inf !{arg:2})])]))] Nothing)
|
||||
Prelude.Types.case block in prim__integerToNat = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%constcase 0 (Builtin.believe_me [___, ___, !{arg:0}])), (%constcase 1 0)] Nothing)
|
||||
Prelude.Types.rangeFrom = [{arg:0}, {arg:1}, {arg:2}]: (Prelude.Types.countFrom [___, !{arg:2}, (%lam {arg:3} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] ((!{e:1} [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:6}, {e:5}, {e:4}] !{e:6})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [1]))] Nothing)]) [!{arg:3}]))] Nothing))])
|
||||
Prelude.Types.rangeFromTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (Prelude.Types.case block in rangeFromTo [___, !{arg:1}, !{arg:2}, !{arg:3}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)])
|
||||
Prelude.Types.rangeFromThen = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (Prelude.Types.case block in rangeFromThen [___, !{arg:1}, !{arg:2}, !{arg:3}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [!{arg:3}]) [!{arg:2}]))] Nothing)])
|
||||
Prelude.Types.rangeFromThenTo = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (Prelude.Types.case block in rangeFromThenTo [___, !{arg:1}, !{arg:2}, !{arg:3}, !{arg:4}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] ((!{e:4} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:2}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:1}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:11}, {e:10}, {e:9}] ((!{e:9} [!{arg:4}]) [!{arg:3}]))] Nothing)]))] Nothing)])
|
||||
Prelude.Types.null = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:2}, {e:3}] (%delay Lazy 1))] Nothing)
|
||||
Prelude.Types.foldr = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%concase Prelude.Types.Nil Just 0 [] !{arg:3}), (%concase Prelude.Types.:: Just 1 [{e:2}, {e:3}] ((!{arg:2} [!{e:2}]) [(Prelude.Types.foldr [___, ___, !{arg:2}, !{arg:3}, !{e:3}])]))] Nothing)
|
||||
Prelude.Types.foldl = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}]: (%case !{arg:4} [(%concase Prelude.Types.Nil Just 0 [] !{arg:3}), (%concase Prelude.Types.:: Just 1 [{e:2}, {e:3}] (Prelude.Types.foldl [___, ___, !{arg:2}, ((!{arg:2} [!{arg:3}]) [!{e:2}]), !{e:3}]))] Nothing)
|
||||
Prelude.Types.Range at Prelude/Types.idr:755:1--761:37 = Constructor tag Just 0 arity 4
|
||||
Prelude.Types.Range implementation at Prelude/Types.idr:787:1--809:48 = [{arg:0}, {arg:1}]: (%con Prelude.Types.Range at Prelude/Types.idr:755:1--761:37 Just 0 [(%lam {arg:5540} (%lam {arg:5541} (Prelude.Types.rangeFromTo [___, !{arg:1}, !{arg:5540}, !{arg:5541}]))), (%lam {arg:5542} (%lam {arg:5543} (%lam {arg:5544} (Prelude.Types.rangeFromThenTo [___, !{arg:1}, !{arg:5542}, !{arg:5543}, !{arg:5544}])))), (%lam {arg:5545} (Prelude.Types.rangeFrom [___, !{arg:1}, !{arg:5545}])), (%lam {arg:5546} (%lam {arg:5547} (Prelude.Types.rangeFromThen [___, !{arg:1}, !{arg:5546}, !{arg:5547}])))])
|
||||
Prelude.Types.Foldable implementation at Prelude/Types.idr:385:1--394:22 = []: (%con Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:227:1--252:55 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:1144} (Prelude.Types.null [___, !{arg:1144}])))])
|
||||
Prelude.Types.takeUntil = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Prelude.Types.Stream.:: Just 0 [{e:1}, {e:2}] (Prelude.Types.case block in takeUntil [___, !{e:1}, !{e:2}, !{arg:1}, (!{arg:1} [!{e:1}])]))] Nothing)
|
||||
Prelude.Types.takeBefore = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Prelude.Types.Stream.:: Just 0 [{e:1}, {e:2}] (Prelude.Types.case block in takeBefore [___, !{e:1}, !{e:2}, !{arg:1}, (!{arg:1} [!{e:1}])]))] Nothing)
|
||||
Prelude.Types.rangeFromTo = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Types.Range at Prelude/Types.idr:755:1--761:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}] (%lam {arg:2} (%lam {arg:3} ((!{e:1} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.Types.prim__integerToNat = [{arg:0}]: (Prelude.Types.case block in prim__integerToNat [!{arg:0}, (%case (<=Integer [0, !{arg:0}]) [(%constcase 0 1)] Just 0)])
|
||||
Prelude.Types.countFrom = [{arg:0}, {arg:1}, {arg:2}]: (%con Prelude.Types.Stream.:: Just 0 [!{arg:1}, (%delay Inf (Prelude.Types.countFrom [___, (!{arg:2} [!{arg:1}]), !{arg:2}]))])
|
||||
Prelude.Types.case block in rangeFromThen = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])), (%constcase 1 (Prelude.Types.countFrom [___, !{arg:N}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))]))] Nothing)
|
||||
Prelude.Types.case block in case block in case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.Nil Just 0 []))] Nothing)
|
||||
Prelude.Types.case block in case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam n (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!n]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in case block in rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (Prelude.Basics.&& [(%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing), (%delay Lazy (%case (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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})] Nothing) [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C Just 0 [{e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing))])]))] Nothing)
|
||||
Prelude.Types.case block in rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeBefore [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)]))] Nothing)
|
||||
Prelude.Types.case block in case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam x (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])]))] Nothing)
|
||||
Prelude.Types.case block in rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Prelude.Types.takeUntil [___, (%lam {arg:N} (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [!{arg:N}]) [!{arg:N}]))] Nothing)), (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]))] Nothing))])])), (%constcase 1 (Prelude.Types.case block in case block in rangeFromTo [___, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)
|
||||
Prelude.Types.case block in takeBefore = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.Nil Just 0 [])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeBefore [___, !{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
|
||||
Prelude.Types.case block in takeUntil = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con Prelude.Types.:: Just 1 [!{arg:N}, (%con Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeUntil [___, !{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
|
||||
Prelude.Types.case block in prim__integerToNat = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (Builtin.believe_me [___, ___, !{arg:N}])), (%constcase 1 0)] Nothing)
|
||||
Prelude.Types.rangeFrom = [{arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.countFrom [___, !{arg:N}, (%lam {arg:N} (%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [(%case (%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] !{e:N})] Nothing) [(%concase Prelude.Num.Num at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing)]) [!{arg:N}]))] Nothing))])
|
||||
Prelude.Types.rangeFromTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromTo [___, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [!{arg:N}]) [!{arg:N}]))] Nothing)])
|
||||
Prelude.Types.rangeFromThen = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromThen [___, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [!{arg:N}]) [!{arg:N}]))] Nothing)])
|
||||
Prelude.Types.rangeFromThenTo = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (Prelude.Types.case block in rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}, (%case (Builtin.fst [___, ___, (Builtin.snd [___, ___, !{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} [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]) [(%case (Builtin.snd [___, ___, (Builtin.snd [___, ___, !{arg:N}])]) [(%concase Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [!{arg:N}]))] Nothing)]))] Nothing)])
|
||||
Prelude.Types.null = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] (%delay Lazy 0)), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (%delay Lazy 1))] Nothing)
|
||||
Prelude.Types.foldr = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] ((!{arg:N} [!{e:N}]) [(Prelude.Types.foldr [___, ___, !{arg:N}, !{arg:N}, !{e:N}])]))] Nothing)
|
||||
Prelude.Types.foldl = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%concase Prelude.Types.Nil Just 0 [] !{arg:N}), (%concase Prelude.Types.:: Just 1 [{e:N}, {e:N}] (Prelude.Types.foldl [___, ___, !{arg:N}, ((!{arg:N} [!{arg:N}]) [!{e:N}]), !{e:N}]))] Nothing)
|
||||
Prelude.Types.Range at Prelude/Types.idr:L:C--L:C = Constructor tag Just 0 arity 4
|
||||
Prelude.Types.Range implementation at Prelude/Types.idr:L:C--L:C = [{arg:N}, {arg:N}]: (%con Prelude.Types.Range at Prelude/Types.idr:L:C--L:C Just 0 [(%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromTo [___, !{arg:N}, !{arg:N}, !{arg:N}]))), (%lam {arg:N} (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThenTo [___, !{arg:N}, !{arg:N}, !{arg:N}, !{arg:N}])))), (%lam {arg:N} (Prelude.Types.rangeFrom [___, !{arg:N}, !{arg:N}])), (%lam {arg:N} (%lam {arg:N} (Prelude.Types.rangeFromThen [___, !{arg:N}, !{arg:N}, !{arg:N}])))])
|
||||
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.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
|
||||
Prelude.Types.Stream.Stream = Constructor tag Nothing arity 1
|
||||
Prelude.Types.Nil = Constructor tag Just 0 arity 0
|
||||
Prelude.Types.:: = Constructor tag Just 1 arity 2
|
||||
Prelude.Types.Stream.:: = Constructor tag Just 0 arity 2
|
||||
Prelude.Num.case block in mod = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 1 (%Int [!{arg:1}, !{arg:0}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in mod at Prelude/Num.idr:116:3--118:40"]))
|
||||
Prelude.Num.case block in div = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 1 (/Int [!{arg:1}, !{arg:0}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in div at Prelude/Num.idr:113:3--115:40"]))
|
||||
Prelude.Num.negate = [{arg:0}]: (-Int [0, !{arg:0}])
|
||||
Prelude.Num.mod = [{arg:0}, {arg:1}]: (Prelude.Num.case block in mod [!{arg:1}, !{arg:0}, (Prelude.EqOrd.== [!{arg:1}, (cast-Integer-Int [0])])])
|
||||
Prelude.Num.fromInteger = [{ext:0}]: (cast-Integer-Int [!{ext:0}])
|
||||
Prelude.Num.div = [{arg:0}, {arg:1}]: (Prelude.Num.case block in div [!{arg:1}, !{arg:0}, (Prelude.EqOrd.== [!{arg:1}, (cast-Integer-Int [0])])])
|
||||
Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Integral at Prelude/Num.idr:48:1--53:23 = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Constraint (Num ty) = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] !{e:1})] Nothing)
|
||||
Prelude.Num.Num implementation at Prelude/Num.idr:95:1--100:38 = []: (%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))])
|
||||
Prelude.Num.Neg implementation at Prelude/Num.idr:102:1--105:22 = []: (%con Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:56} (Prelude.Num.negate [!{arg:56}])), (%lam {arg:57} (%lam {arg:58} (Prelude.Num.- [!{arg:57}, !{arg:58}])))])
|
||||
Prelude.Num.Integral implementation at Prelude/Num.idr:111:1--118:40 = []: (%con Prelude.Num.Integral at Prelude/Num.idr:48:1--53:23 Just 0 [(%con Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [(%lam {arg:2} (%lam {arg:3} (+Int [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (*Int [!{arg:4}, !{arg:5}]))), (%lam {arg:6} (cast-Integer-Int [!{arg:6}]))]), (%lam {arg:184} (%lam {arg:185} (Prelude.Num.div [!{arg:184}, !{arg:185}]))), (%lam {arg:186} (%lam {arg:187} (Prelude.Num.mod [!{arg:186}, !{arg:187}])))])
|
||||
Prelude.Num.- = [{ext:0}, {ext:1}]: (-Int [!{ext:0}, !{ext:1}])
|
||||
Prelude.Num.+ = [{ext:0}, {ext:1}]: (+Int [!{ext:0}, !{ext:1}])
|
||||
Prelude.Num.* = [{ext:0}, {ext:1}]: (*Int [!{ext:0}, !{ext:1}])
|
||||
Prelude.Num.fromInteger = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:2} (!{e:3} [!{arg:2}])))] Nothing)
|
||||
Prelude.Num.- = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Neg at Prelude/Num.idr:26:1--31:23 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:2} (%lam {arg:3} ((!{e:3} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.Num.+ = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:2} (%lam {arg:3} ((!{e:1} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.EqOrd.case block in case block in compare = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 1), (%constcase 1 2)] Nothing)
|
||||
Prelude.EqOrd.case block in compare = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 0), (%constcase 1 (Prelude.EqOrd.case block in case block in compare [!{arg:0}, !{arg:1}, (Prelude.EqOrd.== [!{arg:1}, !{arg:0}])]))] Nothing)
|
||||
Prelude.EqOrd.case block in max = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 !{arg:1}), (%constcase 1 !{arg:0})] Nothing)
|
||||
Prelude.EqOrd.case block in min = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%constcase 0 !{arg:1}), (%constcase 1 !{arg:0})] Nothing)
|
||||
Prelude.EqOrd.min = [{arg:0}, {arg:1}]: (Prelude.EqOrd.case block in min [!{arg:1}, !{arg:0}, (Prelude.EqOrd.< [!{arg:0}, !{arg:1}])])
|
||||
Prelude.EqOrd.max = [{arg:0}, {arg:1}]: (Prelude.EqOrd.case block in max [!{arg:1}, !{arg:0}, (Prelude.EqOrd.> [!{arg:0}, !{arg:1}])])
|
||||
Prelude.EqOrd.compare = [{arg:0}, {arg:1}]: (Prelude.EqOrd.case block in compare [!{arg:1}, !{arg:0}, (Prelude.EqOrd.< [!{arg:0}, !{arg:1}])])
|
||||
Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 = Constructor tag Just 0 arity 8
|
||||
Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 = Constructor tag Just 0 arity 2
|
||||
Prelude.EqOrd.Constraint (Eq ty) = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] !{e:1})] Nothing)
|
||||
Prelude.EqOrd.Ord implementation at Prelude/EqOrd.idr:128:1--135:43 = []: (%con Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [(%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [(%lam {arg:2} (%lam {arg:3} (Prelude.EqOrd.== [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (Prelude.EqOrd./= [!{arg:4}, !{arg:5}])))]), (%lam {arg:371} (%lam {arg:372} (Prelude.EqOrd.compare [!{arg:371}, !{arg:372}]))), (%lam {arg:373} (%lam {arg:374} (Prelude.EqOrd.< [!{arg:373}, !{arg:374}]))), (%lam {arg:375} (%lam {arg:376} (Prelude.EqOrd.> [!{arg:375}, !{arg:376}]))), (%lam {arg:377} (%lam {arg:378} (Prelude.EqOrd.<= [!{arg:377}, !{arg:378}]))), (%lam {arg:379} (%lam {arg:380} (Prelude.EqOrd.>= [!{arg:379}, !{arg:380}]))), (%lam {arg:381} (%lam {arg:382} (Prelude.EqOrd.max [!{arg:381}, !{arg:382}]))), (%lam {arg:383} (%lam {arg:384} (Prelude.EqOrd.min [!{arg:383}, !{arg:384}])))])
|
||||
Prelude.EqOrd.Eq implementation at Prelude/EqOrd.idr:36:1--38:40 = []: (%con Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [(%lam {arg:2} (%lam {arg:3} (Prelude.EqOrd.== [!{arg:2}, !{arg:3}]))), (%lam {arg:4} (%lam {arg:5} (Prelude.EqOrd./= [!{arg:4}, !{arg:5}])))])
|
||||
Prelude.EqOrd.> = [{arg:0}, {arg:1}]: (%case (>Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.>= = [{arg:0}, {arg:1}]: (%case (>=Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.== = [{arg:0}, {arg:1}]: (%case (==Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.< = [{arg:0}, {arg:1}]: (%case (<Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.<= = [{arg:0}, {arg:1}]: (%case (<=Int [!{arg:0}, !{arg:1}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd./= = [{arg:0}, {arg:1}]: (Prelude.Basics.not [(Prelude.EqOrd.== [!{arg:0}, !{arg:1}])])
|
||||
Prelude.Num.case block in mod = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (%Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in mod at Prelude/Num.idr:L:C--L:C"]))
|
||||
Prelude.Num.case block in div = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 1 (/Int [!{arg:N}, !{arg:N}]))] Just (Builtin.idris_crash [___, "Unhandled input for Prelude.Num.case block in div at Prelude/Num.idr:L:C--L:C"]))
|
||||
Prelude.Num.negate = [{arg:N}]: (-Int [0, !{arg:N}])
|
||||
Prelude.Num.mod = [{arg:N}, {arg:N}]: (Prelude.Num.case block in mod [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])])])
|
||||
Prelude.Num.fromInteger = [{ext:N}]: (cast-Integer-Int [!{ext:N}])
|
||||
Prelude.Num.div = [{arg:N}, {arg:N}]: (Prelude.Num.case block in div [!{arg:N}, !{arg:N}, (Prelude.EqOrd.== [!{arg:N}, (cast-Integer-Int [0])])])
|
||||
Prelude.Num.Num at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Neg at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Integral at Prelude/Num.idr:L:C--L:C = Constructor tag Just 0 arity 3
|
||||
Prelude.Num.Constraint (Num ty) = [{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}] !{e:N})] Nothing)
|
||||
Prelude.Num.Num implementation at Prelude/Num.idr:L:C--L:C = []: (%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.Num.Neg implementation at Prelude/Num.idr:L:C--L:C = []: (%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}])))])
|
||||
Prelude.Num.Integral implementation at Prelude/Num.idr:L:C--L:C = []: (%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}])))])
|
||||
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.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)
|
||||
Prelude.EqOrd.case block in min = [{arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N}), (%constcase 1 !{arg:N})] Nothing)
|
||||
Prelude.EqOrd.min = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in min [!{arg:N}, !{arg:N}, (Prelude.EqOrd.< [!{arg:N}, !{arg:N}])])
|
||||
Prelude.EqOrd.max = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in max [!{arg:N}, !{arg:N}, (Prelude.EqOrd.> [!{arg:N}, !{arg:N}])])
|
||||
Prelude.EqOrd.compare = [{arg:N}, {arg:N}]: (Prelude.EqOrd.case block in compare [!{arg:N}, !{arg:N}, (Prelude.EqOrd.< [!{arg:N}, !{arg:N}])])
|
||||
Prelude.EqOrd.Ord at Prelude/EqOrd.idr:L:C--L:C = Constructor tag Just 0 arity 8
|
||||
Prelude.EqOrd.Eq at Prelude/EqOrd.idr:L:C--L:C = Constructor tag Just 0 arity 2
|
||||
Prelude.EqOrd.Constraint (Eq ty) = [{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}] !{e:N})] Nothing)
|
||||
Prelude.EqOrd.Ord implementation at Prelude/EqOrd.idr:L:C--L:C = []: (%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}])))])
|
||||
Prelude.EqOrd.Eq implementation at Prelude/EqOrd.idr:L:C--L:C = []: (%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}])))])
|
||||
Prelude.EqOrd.> = [{arg:N}, {arg:N}]: (%case (>Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.>= = [{arg:N}, {arg:N}]: (%case (>=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case (==Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.< = [{arg:N}, {arg:N}]: (%case (<Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd.<= = [{arg:N}, {arg:N}]: (%case (<=Int [!{arg:N}, !{arg:N}]) [(%constcase 0 1)] Just 0)
|
||||
Prelude.EqOrd./= = [{arg:N}, {arg:N}]: (Prelude.Basics.not [(Prelude.EqOrd.== [!{arg:N}, !{arg:N}])])
|
||||
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:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:6} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.EqOrd.> = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:4} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.EqOrd.== = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Eq at Prelude/EqOrd.idr:13:1--20:24 Just 0 [{e:1}, {e:2}] (%lam {arg:2} (%lam {arg:3} ((!{e:1} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.EqOrd.<= = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:5} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.EqOrd.< = [{arg:0}, {arg:1}]: (%case !{arg:1} [(%concase Prelude.EqOrd.Ord at Prelude/EqOrd.idr:86:1--107:37 Just 0 [{e:1}, {e:2}, {e:3}, {e:4}, {e:5}, {e:6}, {e:7}, {e:8}] (%lam {arg:2} (%lam {arg:3} ((!{e:3} [!{arg:2}]) [!{arg:3}]))))] Nothing)
|
||||
Prelude.Interfaces.Functor at Prelude/Interfaces.idr:67:1--74:38 = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:227:1--252:55 = Constructor tag Just 0 arity 3
|
||||
Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:148:1--151:35 = Constructor tag Just 0 arity 3
|
||||
Prelude.Interfaces.sum = [{arg:0}, {arg:1}, {arg:2}]: (%case (Builtin.fst [___, ___, !{arg:2}]) [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:227:1--252:55 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:3} (((((!{e:1} [___]) [___]) [(%case (Builtin.snd [___, ___, !{arg:2}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (%lam {arg:4} (%lam {arg:5} ((!{e:6} [!{arg:4}]) [!{arg:5}]))))] Nothing)]) [(%case (Builtin.snd [___, ___, !{arg:2}]) [(%concase Prelude.Num.Num at Prelude/Num.idr:16:1--22:30 Just 0 [{e:6}, {e:5}, {e:4}] (!{e:4} [0]))] Nothing)]) [!{arg:3}])))] Nothing)
|
||||
Prelude.Interfaces.pure = [{arg:0}, {arg:1}, {arg:2}]: (%case !{arg:2} [(%concase Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:148:1--151:35 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:3} ((!{e:2} [___]) [!{arg:3}])))] Nothing)
|
||||
Prelude.Interfaces.foldr = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (%case !{arg:3} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:227:1--252:55 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:4} (%lam {arg:5} (%lam {arg:6} (((((!{e:1} [___]) [___]) [!{arg:4}]) [!{arg:5}]) [!{arg:6}])))))] Nothing)
|
||||
Prelude.Interfaces.foldl = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (%case !{arg:3} [(%concase Prelude.Interfaces.Foldable at Prelude/Interfaces.idr:227:1--252:55 Just 0 [{e:1}, {e:2}, {e:3}] (%lam {arg:4} (%lam {arg:5} (%lam {arg:6} (((((!{e:2} [___]) [___]) [!{arg:4}]) [!{arg:5}]) [!{arg:6}])))))] Nothing)
|
||||
PrimIO.case block in unsafePerformIO = [{arg:0}, {arg:1}, {arg:2}, {arg:3}]: (PrimIO.unsafeDestroyWorld [___, ___, !{arg:3}])
|
||||
PrimIO.case block in case block in io_bind = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}, {arg:6}, {arg:7}]: (!{arg:7} [!{arg:6}])
|
||||
PrimIO.case block in io_bind = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {arg:4}, {arg:5}]: (PrimIO.case block in case block in io_bind [___, ___, ___, ___, ___, !{arg:5}, ___, (!{arg:3} [!{arg:5}])])
|
||||
PrimIO.unsafePerformIO = [{arg:0}, {arg:1}]: (PrimIO.unsafeCreateWorld [___, (%lam w (PrimIO.case block in unsafePerformIO [___, !{arg:1}, ___, (!{arg:1} [!w])]))])
|
||||
PrimIO.unsafeDestroyWorld = [{arg:0}, {arg:1}, {arg:2}]: !{arg:2}
|
||||
PrimIO.unsafeCreateWorld = [{arg:0}, {arg:1}]: (!{arg:1} [%MkWorld])
|
||||
PrimIO.io_pure = [{arg:0}, {arg:1}, {ext:0}]: !{arg:1}
|
||||
PrimIO.io_bind = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {ext:0}]: (PrimIO.case block in io_bind [___, ___, ___, !{arg:3}, ___, (!{arg:2} [!{ext: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.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)
|
||||
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}])])
|
||||
PrimIO.unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeCreateWorld [___, (%lam w (PrimIO.case block in unsafePerformIO [___, !{arg:N}, ___, (!{arg:N} [!w])]))])
|
||||
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}, {arg:N}]: !{arg:N}
|
||||
PrimIO.unsafeCreateWorld = [{arg:N}, {arg:N}]: (!{arg:N} [%MkWorld])
|
||||
PrimIO.io_pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
|
||||
PrimIO.io_bind = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (PrimIO.case block in io_bind [___, ___, ___, !{arg:N}, ___, (!{arg:N} [!{ext:N}])])
|
||||
PrimIO.MkIORes = Constructor tag Just 0 arity 3 (newtype by 1)
|
||||
PrimIO.MkIO = Constructor tag Just 0 arity 2 (newtype by 1)
|
||||
Prelude.IO.pure = [{arg:0}, {arg:1}, {ext:0}]: !{arg:1}
|
||||
Prelude.IO.map = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {ext:0}]: (%let {act:3} (!{arg:3} [!{ext:0}]) (!{arg:2} [!{act:3}]))
|
||||
Prelude.IO.Functor implementation at Prelude/IO.idr:15:1--17:46 = [{ext:4}, {ext:1}, {ext:2}, {ext:3}, {ext:0}]: (Prelude.IO.map [___, ___, !{ext:2}, !{ext:3}, !{ext:0}])
|
||||
Prelude.IO.Applicative implementation at Prelude/IO.idr:19:1--26:30 = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:148:1--151:35 Just 0 [(%lam b (%lam a (%lam func (%lam {arg:143} (%lam {eta:0} (Prelude.IO.map [___, ___, !func, !{arg:143}, !{eta:0}])))))), (%lam a (%lam {arg:577} (%lam {eta:0} !{arg:577}))), (%lam b (%lam a (%lam {arg:578} (%lam {arg:580} (%lam {eta:0} (%let {act:17} (!{arg:578} [!{eta:0}]) (%let {act:16} (!{arg:580} [!{eta:0}]) (!{act:17} [!{act:16}]))))))))])
|
||||
Prelude.IO.<*> = [{arg:0}, {arg:1}, {arg:2}, {arg:3}, {ext:0}]: (%let {act:6} (!{arg:2} [!{ext:0}]) (%let {act:5} (!{arg:3} [!{ext:0}]) (!{act:6} [!{act:5}])))
|
||||
Prelude.IO.pure = [{arg:N}, {arg:N}, {ext:N}]: !{arg:N}
|
||||
Prelude.IO.map = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (!{arg:N} [!{act:N}]))
|
||||
Prelude.IO.Functor implementation at Prelude/IO.idr:L:C--L:C = [{ext:N}, {ext:N}, {ext:N}, {ext:N}, {ext:N}]: (Prelude.IO.map [___, ___, !{ext:N}, !{ext:N}, !{ext:N}])
|
||||
Prelude.IO.Applicative implementation at Prelude/IO.idr:L:C--L:C = []: (%con Prelude.Interfaces.Applicative at Prelude/Interfaces.idr:L:C--L:C Just 0 [(%lam b (%lam a (%lam func (%lam {arg:N} (%lam {eta:N} (Prelude.IO.map [___, ___, !func, !{arg:N}, !{eta:N}])))))), (%lam a (%lam {arg:N} (%lam {eta:N} !{arg:N}))), (%lam b (%lam a (%lam {arg:N} (%lam {arg:N} (%lam {eta:N} (%let {act:N} (!{arg:N} [!{eta:N}]) (%let {act:N} (!{arg:N} [!{eta:N}]) (!{act:N} [!{act:N}]))))))))])
|
||||
Prelude.IO.<*> = [{arg:N}, {arg:N}, {arg:N}, {arg:N}, {ext:N}]: (%let {act:N} (!{arg:N} [!{ext:N}]) (%let {act:N} (!{arg:N} [!{ext:N}]) (!{act:N} [!{act:N}])))
|
||||
|
||||
|
||||
@ -1,6 +1,6 @@
|
||||
$1 --no-color --console-width 0 --no-banner --dumpcases Main.cases -o Main Main.idr
|
||||
|
||||
$1 --no-color --console-width 0 --no-banner --exec main CatCases.idr
|
||||
$1 --no-color --console-width 0 --no-banner --exec main CatCases.idr | sed -E "s/[0-9]+}/N}/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g"
|
||||
|
||||
rm -rf build
|
||||
rm Main.cases
|
||||
6
tests/idris2/builtin001/Test.idr
Normal file
6
tests/idris2/builtin001/Test.idr
Normal file
@ -0,0 +1,6 @@
|
||||
|
||||
data MyNat
|
||||
= S MyNat
|
||||
| Z
|
||||
|
||||
%builtin Natural MyNat
|
||||
2
tests/idris2/builtin001/expected
Normal file
2
tests/idris2/builtin001/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building Test (Test.idr)
|
||||
Main> Bye for now!
|
||||
1
tests/idris2/builtin001/input
Normal file
1
tests/idris2/builtin001/input
Normal file
@ -0,0 +1 @@
|
||||
:q
|
||||
3
tests/idris2/builtin001/run
Executable file
3
tests/idris2/builtin001/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --no-color --console-width 0 --no-banner Test.idr < input
|
||||
|
||||
rm -rf build
|
||||
6
tests/idris2/builtin002/Test.idr
Normal file
6
tests/idris2/builtin002/Test.idr
Normal file
@ -0,0 +1,6 @@
|
||||
|
||||
data MyNat
|
||||
= S MyNat MyNat
|
||||
| Z
|
||||
|
||||
%builtin Natural MyNat
|
||||
12
tests/idris2/builtin002/expected
Normal file
12
tests/idris2/builtin002/expected
Normal file
@ -0,0 +1,12 @@
|
||||
1/1: Building Test (Test.idr)
|
||||
Error: Constructor Main.S doesn't match any pattern for Natural.
|
||||
|
||||
Test.idr:6:1--6:23
|
||||
2 | data MyNat
|
||||
3 | = S MyNat MyNat
|
||||
4 | | Z
|
||||
5 |
|
||||
6 | %builtin Natural MyNat
|
||||
^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
Main> Bye for now!
|
||||
1
tests/idris2/builtin002/input
Normal file
1
tests/idris2/builtin002/input
Normal file
@ -0,0 +1 @@
|
||||
:q
|
||||
3
tests/idris2/builtin002/run
Executable file
3
tests/idris2/builtin002/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --no-color --console-width 0 --no-banner Test.idr < input
|
||||
|
||||
rm -rf build
|
||||
6
tests/idris2/builtin003/Test.idr
Normal file
6
tests/idris2/builtin003/Test.idr
Normal file
@ -0,0 +1,6 @@
|
||||
|
||||
data Fin : Nat -> Type where
|
||||
FS : Fin k -> Fin (S k)
|
||||
FZ : Fin (S k)
|
||||
|
||||
%builtin Natural Fin
|
||||
2
tests/idris2/builtin003/expected
Normal file
2
tests/idris2/builtin003/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building Test (Test.idr)
|
||||
Main> Bye for now!
|
||||
1
tests/idris2/builtin003/input
Normal file
1
tests/idris2/builtin003/input
Normal file
@ -0,0 +1 @@
|
||||
:q
|
||||
3
tests/idris2/builtin003/run
Executable file
3
tests/idris2/builtin003/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --no-color --console-width 0 --no-banner Test.idr < input
|
||||
|
||||
rm -rf build
|
||||
6
tests/idris2/builtin004/Test.idr
Normal file
6
tests/idris2/builtin004/Test.idr
Normal file
@ -0,0 +1,6 @@
|
||||
|
||||
data MyNat
|
||||
= S (Inf MyNat)
|
||||
| Z
|
||||
|
||||
%builtin Natural MyNat
|
||||
12
tests/idris2/builtin004/expected
Normal file
12
tests/idris2/builtin004/expected
Normal file
@ -0,0 +1,12 @@
|
||||
1/1: Building Test (Test.idr)
|
||||
Error: Natural builtin does not support lazy types, as they can be potentially infinite.
|
||||
|
||||
Test.idr:6:1--6:23
|
||||
2 | data MyNat
|
||||
3 | = S (Inf MyNat)
|
||||
4 | | Z
|
||||
5 |
|
||||
6 | %builtin Natural MyNat
|
||||
^^^^^^^^^^^^^^^^^^^^^^
|
||||
|
||||
Main> Bye for now!
|
||||
1
tests/idris2/builtin004/input
Normal file
1
tests/idris2/builtin004/input
Normal file
@ -0,0 +1 @@
|
||||
:q
|
||||
3
tests/idris2/builtin004/run
Executable file
3
tests/idris2/builtin004/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --no-color --console-width 0 --no-banner Test.idr < input
|
||||
|
||||
rm -rf build
|
||||
Loading…
Reference in New Issue
Block a user