gallery (why3doc now called externally)

parent 4d693c03
......@@ -360,23 +360,22 @@ install_local: bin/why3ml
# gallery
##########
%.gallery: %.mlw bin/why3doc
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
mkdir -p $(GALLERYDIR)/`basename $*`
bin/why3doc -b -o $(GALLERYDIR)/`basename $*` $*.mlw
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
power mergesort_list mac_carthy isqrt insertion_sort_list flag \
distance muller \
distance muller fib_memo fibonacci \
vstte10_aqueue vstte10_inverting vstte10_max_sum \
vstte10_queens vstte10_search_list \
vacid_0_sparse_array
GALLERYFILES = $(addprefix examples/programs/, $(GALLERYPGMS))
GALLERY = $(addsuffix .gallery, $(GALLERYFILES))
.PHONY: gallery
gallery:: $(GALLERY)
gallery::
@if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi
@for f in $(GALLERYPGMS); do \
echo "exporting $$f"; \
mkdir -p $(GALLERYDIR)/$$f; \
cp examples/programs/$$f.mlw $(GALLERYDIR)/$$f/; \
done
########
# Config
......@@ -722,6 +721,9 @@ bin/why3doc.byte: src/why.cma $(WHY3DOCCMO)
bin/why3doc: bin/why3doc.@OCAMLBEST@
ln -sf why3doc.@OCAMLBEST@ $@
install_no_local::
cp -f bin/why3doc.@OCAMLBEST@ $(BINDIR)/why3doc
# depend and clean targets
WHY3DOCGENERATED=src/why3doc/to_html.ml
......
(* Fibonacci function with memoisation *)
module M
use import int.Int
use import module stdlib.Ref
(* Fibonacci function with memoisation *)
(*
logic fib (n:int) : int =
if n <= 1 then 1 else fib (n-1) + fib (n-2)
*)
logic fib int : int
axiom Fib_def : forall n:int. fib n =
......@@ -24,34 +19,34 @@ module M
logic inv (t : table) =
forall x y : int. A.get t x = Some y -> y = fib x
parameter table : ref table
parameter table : ref table
parameter add :
x:int -> y:int ->
{} unit writes table { table = A.set (old table) x (Some y) }
parameter add :
x:int -> y:int ->
{} unit writes table { table = A.set (old table) x (Some y) }
exception Not_found
exception Not_found
parameter find :
x:int ->
{}
int reads table raises Not_found
{ A.get table x = Some result }
| Not_found -> { A.get table x = None }
parameter find :
x:int ->
{}
int reads table raises Not_found
{ A.get table x = Some result }
| Not_found -> { A.get table x = None }
let rec fibo n =
{ 0 <= n and inv table }
if n <= 1 then
1
else
memo_fibo (n-1) + memo_fibo (n-2)
{ result = fib n and inv table }
with memo_fibo n =
{ 0 <= n and inv table }
try find n
with Not_found -> let fn = fibo n in add n fn; fn end
{ result = fib n and inv table }
let rec fibo n =
{ 0 <= n and inv table }
if n <= 1 then
1
else
memo_fibo (n-1) + memo_fibo (n-2)
{ result = fib n and inv table }
with memo_fibo n =
{ 0 <= n and inv table }
try find n
with Not_found -> let fn = fibo n in add n fn; fn end
{ result = fib n and inv table }
end
......
......@@ -7,10 +7,9 @@ theory Fibonacci
| isfib0: isfib 0 0
| isfib1: isfib 1 1
| isfibn:
forall n r p: int.
n >= 2 && isfib (n-2) r && isfib (n-1) p -> isfib n (p+r)
forall n r p: int.
n >= 2 && isfib (n-2) r && isfib (n-1) p -> isfib n (p+r)
lemma isfib_2_1 : isfib 2 1
lemma isfib_6_8 : isfib 6 8
......
......@@ -42,7 +42,6 @@ let do_file env fname =
let m = Env.read_file env fname in
let base =
let f = Filename.basename fname in
let f = try Filename.chop_extension f with _ -> f in
match !opt_output with
| None -> f
| Some dir -> Filename.concat dir f
......
......@@ -166,7 +166,6 @@ div.sig_block {margin-left: 2em}";
(* output *)
let f = Filename.basename fname in
let base =
let f = try Filename.chop_extension f with _ -> f in
match !opt_output with
| None -> f
| Some dir -> Filename.concat dir f
......
Markdown is supported
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