Library All

Require Export ProdFunctors.
Require Export SumFunctors.
Require Export ListFunctors.
Require Export FiniteSetLat.
Require Export MapFunctors.

Require Export FlatPos.
Require Export Interval.

Require Export LatticeWidenOfLatticeWf.
Require Export SolveWf.
Require Export SolveWiden.

Module Wf.

Module ZSet <: SetSimplSign.
  Definition t := Z.
  Definition eq_dec := Z_eq_dec.
End ZSet.

Module ZSetSign := SetSign_of_SetSimplSign ZSet.
Module Num <: LatticeWf := FlatLattice ZSetSign.

Module Ref <: LatticeWf := FiniteSetLatticeWf.

Module Val <: LatticeWf := SumLiftLatticeWf Num Ref.

Module LocalVar <: LatticeWf := ArrayBinLatticeWf Val.

Module OperandStack <: LatticeWf := ListLiftLatticeWf Val.

Module Heap' <: LatticeWf := ArrayBinLatticeWf Val.
Module Heap <: LatticeWf := ArrayBinLatticeWf Heap'.

Module State' <: LatticeWf := ProdLatticeWf LocalVar Heap.
Module State <: LatticeWf := ProdLatticeWf OperandStack State'.

Module Context' <: FiniteSet := ProdFiniteSet WordFiniteSet WordFiniteSet.

Module N5 <: NAT.
 Definition val : nat := (5)%nat.
End N5.

Module Context <: FiniteSet := ListFiniteSet N5 Context'.

Module ContextOT <: FiniteSetOT := FiniteSetOT_Of_FiniteSet Context.

Module Map := FMapList.Make ContextOT.OT.
Module GlobalState <: LatticeWf := MapLatticeWf ContextOT Map State.

End Wf.

Module Widen.

Module Num <: LatticeWiden := IntervalLattice.

Module Ref' <: LatticeWf := FiniteSetLatticeWf.
Module Ref <: LatticeWiden := LatticeWiden_Of_LatticeWf Ref'.

Module Val <: LatticeWiden := SumLiftLatticeWiden Num Ref.

Module LocalVar <: LatticeWiden := ArrayBinLatticeWiden Val.

Module OperandStack <: LatticeWiden := ListLiftLatticeWiden Val.

Module Heap' <: LatticeWiden := ArrayBinLatticeWiden Val.
Module Heap <: LatticeWiden := ArrayBinLatticeWiden Heap'.

Module State' <: LatticeWiden := ProdLatticeWiden LocalVar Heap.
Module State <: LatticeWiden := ProdLatticeWiden OperandStack State'.

Module Context' <: FiniteSet := ProdFiniteSet WordFiniteSet WordFiniteSet.

Module N5 <: NAT.
 Definition val : nat := (5)%nat.
End N5.

Module Context <: FiniteSet := ListFiniteSet N5 Context'.

Module ContextOT <: FiniteSetOT := FiniteSetOT_Of_FiniteSet Context.

Module Map := FMapList.Make ContextOT.OT.
Module GlobalState <: LatticeWiden := MapLatticeWiden ContextOT Map State.

End Widen.
Index
This page has been generated by coqdoc