Module LinearizeBackend

Require Import ImpureConfig.
Require Import ASTerm.
Require Import ZNoneItv.
Require Import LinTerm.

Record linearizeContext: Type := {
  nonaffine: ZTerm.t;
  env: PVar.t -> ZNItv.t;
  affine: ZAffTerm.t;
  source: ZTerm.t;
  cmp: cmpG
}.

The oracle is expected to return a polynomial which equals to lc.nonaffine.

Axiom oracle: linearizeContext -> imp ZTerm.t.