Commit b032b78a authored by Arthur Correnson's avatar Arthur Correnson Committed by François Bobot
Browse files

fix Coq documentation generation

parent 370f076a
......@@ -10,4 +10,4 @@ cleandoc:
doc:
@ mkdir -p doc
@ coq2html -base F *.v *.glob -d doc -redirect
\ No newline at end of file
@ cd thry && coq2html -base F -d ../doc *.v *.glob
\ No newline at end of file
# Farith2
Farith2 is an *under construction* Coq module formalizing floating points abstract domains based on [Flocq](http://flocq.gforge.inria.fr/).
## Structure
The structure of the sources may vary a lot over time. For now the structure is as follows :
+ the folder `thry` contains all Coq modules
+ the folder `farith_big` contains OCaml modules used to provide a compatibility layer with Zarith for efficient extraction
+ the `extract.v` file drives the extraction to OCaml
+ the root contains `.ml(i)` files generated by extraction
## Compilation
The compilation of the Coq sources is handled with CoqMakefile. To compile everything, simply type `make` at Farith2's root.
To generate the documentation, it is first required to build the sources using `make` and then `make doc` should fill the `doc` folder with the html documentation formatted using [coq2html](https://github.com/xavierleroy/coq2html).
\ No newline at end of file
-R ./thry F
./thry/Interval.v
./thry/All.v
./thry/Intv32.v
./thry/Tactics.v
./thry/Rextended.v
......
function toggleDisplay(id)
{
var elt = document.getElementById(id);
if (elt.style.display == 'none') {
elt.style.display = 'block';
} else {
elt.style.display = 'none';
}
}
function hideAll(cls)
{
var testClass = new RegExp("(^|s)" + cls + "(s|$)");
var tag = tag || "*";
var elements = document.getElementsByTagName("div");
var current;
var length = elements.length;
for(var i=0; i<length; i++){
current = elements[i];
if(testClass.test(current.className)) {
current.style.display = 'none';
}
}
}
(** * A list of all submodules of Farith2 *)
(** Usefull facts about floating points *)
From F Require Import Utils.
(** An extension of [R] including infinite values
together with a new semantic for floating points
*)
From F Require Import Rextended.
(** An extension of [Q] including infinite values
used to write the specifications of conversions from [Q] to [float]
and from [float] to [Q]
*)
From F Require Import Qextended.
(** Correction lemmas associated to floating point binary operators *)
From F Require Import Utils.
(** A 32 bits instanciation of Flocq's [BinarySingleNaN] *)
From F Require Import B32.
(** Generic float intervals with verified propagators *)
From F Require Import Interval.
(** A 32 bits instanciation of [Interval] *)
From F Require Import Intv32.
\ No newline at end of file
......@@ -67,11 +67,10 @@ Ltac ieasy :=
Ltac sdestruct x :=
try destruct x; simpl; easy.
Program Definition inter (I1 I2 : Interval) : Interval_opt :=
inter' I1 I2.
Next Obligation with auto.
Next Obligation.
destruct I1 as [[|lo1 hi1 nan1] H1], I2 as [[|lo2 hi2 nan2] H2]; ieasy; try (now destruct nan1 || now destruct nan2).
case (Bltb (hi1) (lo2)) eqn:?, (Bltb (hi2) (lo1)) eqn:?; simpl; try (destruct nan1, nan2; simpl; easy).
pose proof (le_not_nan_l _ _ H1).
......@@ -150,8 +149,8 @@ Definition Iadd' (m : mode) (I1 I2 : Interval') : Interval' :=
Program Definition Iadd (m : mode) (I1 I2 : Interval) : Interval :=
Iadd' m I1 I2.
Next Obligation with auto.
destruct I1 as [[|l1 h1] H1], I2 as [[|l2 h2] H2]; simpl in *...
Next Obligation.
destruct I1 as [[|l1 h1] H1], I2 as [[|l2 h2] H2]; simpl in *; auto.
destruct (is_nan (Bplus m l1 l2)) eqn:E1, (is_nan (Bplus m h1 h2)) eqn:E2; try easy; simpl.
apply B2Rx_le; auto.
repeat (rewrite Bplus_correct; auto).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment