Skip to content
This repository has been archived by the owner on Oct 18, 2021. It is now read-only.

Reduce is not inlining an atom #264

Closed
SquidDev opened this issue Jan 26, 2020 · 1 comment · May be fixed by #265
Closed

Reduce is not inlining an atom #264

SquidDev opened this issue Jan 26, 2020 · 1 comment · May be fixed by #265
Labels
bug Optimiser Issues and PRs relating to the optimiser X-Core Lint Core lint errors in type-checked code.

Comments

@SquidDev
Copy link
Member

Attempting to compile this file with --core-lint fails with the following error:

external val (+) : int -> int -> int = "function(x, y) return x + y end"

type sz_tree =
  | E
  | T of sz_tree * sz_tree

let rec foldr f zero = function
  | E -> zero
  | T (l, r) -> foldr f (f (foldr f zero r)) l

let _ = foldr (1+) 0 E
+#v161 : (| int#t-2, int#t-2 |) -> int#t-2 = foreign
type sz_tree#t2 {
  E#D3 : sz_tree#t2;
  T#D4 : {_1 : sz_tree#t2, _2 : sz_tree#t2} -> sz_tree#t2
}
let gb#v183 : unit#t-5 =
  let fy#v180 : int#t-2 -> int#t-2 =
    λ (gf#v187 : int#t-2).
      let gg#v188 : (| int#t-2, int#t-2 |) =
        (# 1, gf#v187:[int#t-2] #)
      in +#v161:[(| int#t-2, int#t-2 |) -> int#t-2] gg#v188:[(| int#t-2, int#t-2 |)]
  in let rec             
    foldr_sat#v204 : int#t-2 -> sz_tree#t2 -> int#t-2 =
      λ (zero#v205 : int#t-2).
        λ (x#v206 : sz_tree#t2).
          match x#v206:[sz_tree#t2] {
            (T#D4 gz#v207:[{_1 : sz_tree#t2, _2 : sz_tree#t2}]) [] : sz_tree#t2 ->
              match gz#v207:[{_1 : sz_tree#t2, _2 : sz_tree#t2}] {
                {_1 = l#v209:[sz_tree#t2], _2 = r#v208:[sz_tree#t2]} [] : {_1 : sz_tree#t2, _2 : sz_tree#t2} ->
                  let gk#v216 : sz_tree#t2 -> int#t-2 =
                    (* XXX No such variable zero#v196 *)
                    foldr_sat#v204:[int#t-2 -> sz_tree#t2 -> int#t-2] zero#v196:[int#t-2]
                  in let hj#v217 : int#t-2 =
                    gk#v216:[sz_tree#t2 -> int#t-2] r#v208:[sz_tree#t2]
                  in let hk#v218 : int#t-2 =
                    fy#v180:[int#t-2 -> int#t-2] hj#v217:[int#t-2]
                  in let gk#v219 : sz_tree#t2 -> int#t-2 =
                    foldr_sat#v204:[int#t-2 -> sz_tree#t2 -> int#t-2] hk#v218:[int#t-2]
                  in gk#v219:[sz_tree#t2 -> int#t-2] l#v209:[sz_tree#t2]
              };
            E#D3 [] : sz_tree#t2 ->
              zero#v205:[int#t-2]
          }
  in let ga#v182 : sz_tree#t2 -> int#t-2 =
    foldr_sat#v204:[int#t-2 -> sz_tree#t2 -> int#t-2] 0
  in let gc#v184 : int#t-2 =
    ga#v182:[sz_tree#t2 -> int#t-2] E#D3:[sz_tree#t2]
  in unit

Effectively, in a previous pass we generate a binding let zero#v196 = 0 which should be inlined everywhere, and so the binding is automatically removed. However, somehow we're not visiting all nodes, and so this term isn't inlined everywhere.

@SquidDev SquidDev added bug X-Core Lint Core lint errors in type-checked code. Optimiser Issues and PRs relating to the optimiser labels Jan 26, 2020
@SquidDev
Copy link
Member Author

Minor update: apparently we're generating let zero#v196 = zero#v196:['a#'t84] somehow. This is obviously not a very well formed piece of code.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Optimiser Issues and PRs relating to the optimiser X-Core Lint Core lint errors in type-checked code.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant