Abbrevs.v 1.77 KB
Newer Older
1
(**
2
  This file contains some type abbreviations, to ease writing.
3
 **)
4
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
5
Require Import Daisy.Infra.MachineType.
6 7

Global Set Implicit Arguments.
8
(**
9 10 11 12 13 14 15 16
We define Intervals twice.
First we define intervals of reals and fractions.
We need both of them since the analysis argues about intervals of fractions
and the proofs should argue about real valued exections.

Intervals are defined as a type, consisting of a pair of two real numbers or fractions.
Additionally add some constructing and destructing definitions for encapsulation and
define them to automatically unfold upon simplification.
17 18
 **)
Definition interval:Type := R * R.
19
Definition err:Type := R.
20 21 22
Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
Definition IVlo (intv:interval) := fst intv.
Definition IVhi (intv:interval) := snd intv.
23

24
Arguments mkInterval _ _/.
Heiko Becker's avatar
Heiko Becker committed
25 26 27
Arguments IVlo _ /.
Arguments IVhi _ /.

Heiko Becker's avatar
Heiko Becker committed
28 29 30
Definition intv:Type := Q * Q.
Definition error :Type := Q.

31 32 33 34 35 36 37 38
Definition mkIntv (ivlo:Q) (ivhi:Q) := (ivlo,ivhi).
Definition ivlo (intv:intv) := fst intv.
Definition ivhi (intv:intv) := snd intv.

Arguments mkIntv _ _/.
Arguments ivlo _ /.
Arguments ivhi _ /.

39
(**
40 41
  Later we will argue about program preconditions.
  Define a precondition to be a function mapping numbers (resp. variables) to intervals.
42
**)
43
Definition precond :Type := nat -> intv.
44 45

(**
46
  Abbreviation for the type of a variable environment, which should be a partial function
47
 **)
48
Definition env := nat -> option R.
49

50 51 52
(**
  The empty environment must return NONE for every variable
**)
53
Definition emptyEnv:env := fun _ => None.
54

55
(**
56
  Define environment update function as abbreviation, for variable environments
57
**)
58
Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
59
  if (y =? x) 
60
  then Some v
='s avatar
= committed
61
  else E y.