idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

[ fix #1378 ] Collect constructors after inlining (#1380)

Browse Source
This commit is contained in:
Zoe Stafford 2021-05-10 11:19:18 +01:00 committed by GitHub
parent 8038f0a0f9
commit 25ae664ef6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 12 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Compiler/Inline.idr
View File

@ -436,7 +436,7 @@ mutual
addRefs ds (CLam _ _ sc) = addRefs ds sc
addRefs ds (CLet _ _ _ val sc) = addRefs (addRefs ds val) sc
addRefs ds (CApp _ f args) = addRefsArgs (addRefs ds f) args
addRefs ds (CCon _ _ _ _ args) = addRefsArgs ds args
addRefs ds (CCon _ n _ _ args) = addRefsArgs (insert n False ds) args
addRefs ds (COp _ _ args) = addRefsArgs ds (toList args)
addRefs ds (CExtPrim _ _ args) = addRefsArgs ds args
addRefs ds (CForce _ _ e) = addRefs ds e
@ -473,7 +473,7 @@ inlineDef : {auto c : Ref Ctxt Defs} ->
inlineDef n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
let Just cexpr = compexpr def | Nothing => pure ()
setCompiled n !(inline n cexpr)
-- Update the names a function refers to at runtime based on the transformation

10
tests/codegen/con001/expected
View File

@ -8,6 +8,7 @@ Builtin.snd = [{arg:N}]: (%case !{arg:N} [(%concase [cons] Builtin.MkPair Just 0
Builtin.idris_crash = [{ext:N}]: (crash [___, !{ext:N}])
Builtin.fst = [{arg:N}]: (%case !{arg:N} [(%concase [cons] Builtin.MkPair Just 0 [{e:N}, {e:N}] !{e:N})] Nothing)
Builtin.believe_me = [{ext:N}]: (believe_me [___, ___, !{ext:N}])
Builtin.MkPair = Constructor tag Just 0 arity 2
Prelude.Types.case block in case block in rangeFromTo = [{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.MkOrd 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.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!x]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] Nothing))])])), (%constcase 1 (%con [cons] Prelude.Types.:: Just 1 [!{arg:N}, (%con [nil] Prelude.Types.Nil Just 0 [])]))] Nothing)
Prelude.Types.case block in rangeFromTo = [{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.MkOrd 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 (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{arg:N}]) [(%case (Builtin.snd [(Builtin.snd [!{arg:N}])]) [(%concase Prelude.Num.MkNeg Just 0 [{e:N}, {e:N}, {e:N}] (%case !{e:N} [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [1]))] Nothing))] Nothing)]))] 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.MkOrd 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 takeUntil = [{arg:N}, {arg:N}, {arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 (%con [cons] Prelude.Types.:: Just 1 [!{arg:N}, (%con [nil] Prelude.Types.Nil Just 0 [])])), (%constcase 1 (%con [cons] Prelude.Types.:: Just 1 [!{arg:N}, (Prelude.Types.takeUntil [!{arg:N}, (%force Inf !{arg:N})])]))] Nothing)
@ -20,12 +21,18 @@ Prelude.Types.foldlM = [{arg:N}, {arg:N}, {arg:N}, {ext:N}]: (Prelude.Types.fold
Prelude.Types.takeUntil = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%concase [cons] 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.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}]: (%con [cons] Prelude.Types.Stream.:: Just 0 [!{arg:N}, (%delay Inf (Prelude.Types.countFrom [(!{arg:N} [!{arg:N}]), !{arg:N}]))])
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: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.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.- = [{ext:N}, {ext:N}]: (-Int [!{ext:N}, !{ext:N}])
Prelude.Num.MkNum = Constructor tag Just 0 arity 3
Prelude.Num.MkNeg = Constructor tag Just 0 arity 3
Prelude.Num.MkIntegral = Constructor tag Just 0 arity 3
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)
@ -39,7 +46,10 @@ Prelude.EqOrd.== = [{arg:N}, {arg:N}]: (%case (==Int [!{arg:N}, !{arg:N}]) [(%co
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 (Prelude.EqOrd.== [!{arg:N}, !{arg:N}]) [(%constcase 0 1), (%constcase 1 0)] Nothing)
Prelude.EqOrd.MkOrd = Constructor tag Just 0 arity 8
Prelude.EqOrd.MkEq = Constructor tag Just 0 arity 2
Prelude.Interfaces.sum = [{arg:N}, {ext:N}]: (%case (Builtin.fst [!{arg:N}]) [(%concase Prelude.Interfaces.MkFoldable Just 0 [{e:N}, {e:N}, {e:N}, {e:N}] (((((!{e:N} [___]) [___]) [(%lam {eta:N} (%lam {eta:N} (%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] ((!{e:N} [!{eta:N}]) [!{eta:N}]))] Nothing)))]) [(%case (Builtin.snd [!{arg:N}]) [(%concase Prelude.Num.MkNum Just 0 [{e:N}, {e:N}, {e:N}] (!{e:N} [0]))] Nothing)]) [!{ext:N}]))] Nothing)
Prelude.Interfaces.MkFoldable = Constructor tag Just 0 arity 4
PrimIO.case block in unsafePerformIO = [{arg:N}, {arg:N}]: (PrimIO.unsafeDestroyWorld [___, !{arg:N}])
PrimIO.unsafePerformIO = [{arg:N}]: (PrimIO.unsafeCreateWorld [(%lam w (PrimIO.case block in unsafePerformIO [!{arg:N}, (!{arg:N} [!w])]))])
PrimIO.unsafeDestroyWorld = [{arg:N}, {arg:N}]: !{arg:N}