RuleTransform.v

Program Fixpoint rule_transform `{UInverse opu} `{BInverse opb} (p : pro) (free_nominals : Stream nat) (ed : eqn) {measure (complexity p ed)} : EnvT failure (Stream nat) (list eqn) :=
  if orb (is_alpha p ed) (is_beta p ed) then (free_nominals, succ: ([ed])) else
    let av := ed.(a) in
    let bv := ed.(b) in
    match (av, bv, (bmf_pure_in p av, bmf_pure_in p bv)) with
    | (b_conj a1 a2, o, (false, _)) | (o, b_conj a1 a2, (_, false)) => (* /\ rule *)
                                      recurse free_nominals (rule_transform p) [{|a := a1; b := o|}; {|a := a2; b := o|}]
    | (b_negnom x, b_diab o a1 a2, (_, false)) | (b_diab o a1 a2, b_negnom x, (false, _)) => (* binary dia rule *)
                                                 let (n1, n2) := (inr (free_nominals 0) : nom + nat, inr (free_nominals 1)) in (* if the type in there is not explicitly annotated coq inferrs something else which causes a universe inconsistency in the end *)
                                                 fmap (fun r => {|a := b_negnom x; b := diab o (b_nom n1) (b_nom n2)|} :: r) (recurse (advance 2 free_nominals) (rule_transform p) [{|a:=b_negnom n1;b:=a1|}; {|a:=b_negnom n2;b:=a2|}])
    | (b_diau o a1, b_negnom x, (false, _)) | (b_negnom x, b_diau o a1, (_, false)) => (* unary dia rule *)
                                              let n1 := inr (free_nominals 0) : nom + nat in
                                              fmap (fun r => {|a := b_negnom x; b := b_diau o (b_nom n1)|} :: r) (rule_transform p (advance 1 free_nominals) {|a:=b_negnom n1;b:=a1|})
    | (b_disj a1 a2, f, (false, true)) | (f, b_disj a1 a2, (true, false)) =>
                                         let a1pp := bmf_pure_in p a1 in
                                         let a2pp := bmf_pure_in p a2 in
                                         match (a1pp, a2pp) with
                                         | (true, false) => rule_transform p free_nominals {|a:=a2;b:= b_disj a1 f |}
                                         | (false, true) => rule_transform p free_nominals {|a:=a1;b:= b_disj f a2 |}
                                         | _ => (free_nominals, fail: ([ed]))
                                         end
    | (f, b_boxu o a1, (true, false)) | (b_boxu o a1, f, (false, true)) =>
                                    rule_transform p free_nominals {|a:=a1;b:=boxui o f|}
    | (b_boxb o a1 a2, f, (_, true)) | (f, b_boxb o a1 a2, (true, _)) =>
                                       let a1pp := bmf_pure_in p a1 in
                                       let a2pp := bmf_pure_in p a2 in
                                       match (a1pp, a2pp) with
                                       | (true, false) => rule_transform p free_nominals {|a:=a2;b:=boxbi o false a1 f|}
                                       | (false, true) => rule_transform p free_nominals {|a:=a1;b:=boxbi o true f a2|}
                                       | _ => (free_nominals, fail: ([ed]))
                                       end
    | (_, _, (_, _)) => (free_nominals, fail: ([ed]))
    end.