ExpressionAbbrevs.v 901 Bytes
Newer Older
1
(**
2 3
  Some abbreviations that require having defined expressions beforehand
  If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
4
**)
Heiko Becker's avatar
Heiko Becker committed
5
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts.
6 7
Require Export Daisy.Infra.Abbrevs Daisy.Expressions.

Heiko Becker's avatar
Heiko Becker committed
8 9 10 11 12 13 14 15 16

Module Q_orderedExps := ExpOrderedType (Q_as_OT).
Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).

Module DaisyMap := FMapAVL.Make(legacy_OrderedQExps).
Module DaisyMapFacts := OrdProperties (DaisyMap).

Definition analysisResult :Type := DaisyMap.t (intv * error).

17 18 19 20
(**
We treat a function mapping an expression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
Heiko Becker's avatar
Heiko Becker committed
21
(* Definition analysisResult :Type := exp Q -> intv * error. *)