Module Backend

Require Import String.
Require Import NumC.
Require Import ProgVar.
Require Import LinTerm.
Require Import CstrC.
Require Import CertC.
Require Import ConsSet.
Require Export ImpureConfig.

Axiom t: Set.

Inductive bndT: Set
:=
  | Infty: bndT
  | Open: QNum.t -> Cert.frag_t -> bndT
  | Closed: QNum.t -> Cert.frag_t -> bndT.

Record itvT: Set
:= mk {
       low: bndT;
       up: bndT
}.

Inductive addPrecT: Set
  := Added: t -> Cert.t * Cert.t -> addPrecT
   | Contrad: Cert.t -> addPrecT.

Axiom freshId: t -> imp Cert.id_t.
Axiom top: t.
Axiom isEmpty: t -> imp (option Cert.t).
Axiom isIncl: t * t -> imp (option Cert.t).
Axiom add: t * Cstr.t -> imp (option t * Cert.t).
Axiom addp: t * Cstr.t -> imp addPrecT.
Axiom meet: t * t -> imp (option t * Cert.meetT).
Axiom join: t * t -> imp (t * Cert.joinT).
Axiom widen: t * t -> imp (t * Cs.t).
Axiom getItv: t * LinQ.t -> imp itvT.
Axiom getUpperBound: t * LinQ.t -> imp bndT.
Axiom getLowerBound: t * LinQ.t -> imp bndT.
Axiom project: t * PVar.t -> imp (t * Cert.t).
Axiom rename: PVar.t * PVar.t * t -> imp t.
Axiom pr: t -> string.