skip constructor: expr_fvs

[sweirich]

expr_fvs :: CoreExpr -> FV
expr_fvs (Type ty) fv_cand in_scope acc =
  tyCoFVsOfType ty fv_cand in_scope acc
expr_fvs (Coercion co) fv_cand in_scope acc =
  tyCoFVsOfCo co fv_cand in_scope acc
expr_fvs (Var var) fv_cand in_scope acc = FV.unitFV var fv_cand in_scope acc
expr_fvs (Lit _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
expr_fvs (Tick t expr) fv_cand in_scope acc =
  (tickish_fvs t `unionFV` expr_fvs expr) fv_cand in_scope acc
expr_fvs (App fun arg) fv_cand in_scope acc =
  (expr_fvs fun `unionFV` expr_fvs arg) fv_cand in_scope acc
...

Doesn't remove the entire case, just the part of the pattern. This one is pretty serious as it is a function we prove stuff about.

Definition expr_fvs : Core.CoreExpr -> FV.FV :=
  fix expr_fvs arg_0__ arg_1__ arg_2__ arg_3__
        := match arg_0__, arg_1__, arg_2__, arg_3__ with
           | fv_cand, in_scope, acc => FV.emptyFV fv_cand in_scope acc
           | fv_cand, in_scope, acc => FV.emptyFV fv_cand in_scope acc
           | Core.Mk_Var var, fv_cand, in_scope, acc => FV.unitFV var fv_cand in_scope acc
           | Core.Lit _, fv_cand, in_scope, acc => FV.emptyFV fv_cand in_scope acc
           | fv_cand, in_scope, acc =>
               (FV.unionFV FV.emptyFV (expr_fvs expr)) fv_cand in_scope acc
           | Core.App fun_ arg, fv_cand, in_scope, acc =>
               (FV.unionFV (expr_fvs fun_) (expr_fvs arg)) fv_cand in_scope acc
           | Core.Lam bndr body, fv_cand, in_scope, acc =>
               addBndr bndr (expr_fvs body) fv_cand in_scope acc
           | fv_cand, in_scope, acc =>
               (FV.unionFV (expr_fvs expr) FV.emptyFV) fv_cand in_scope acc

[antalsz]

I think this is a duplicate of #132, but I’ll leave it open until I confirm that.

[sweirich]

Thanks. This is is the most serious one. I don't want to replace it with a redefine or an axiomatize.