...
 
Commits (52)
Arthur Charguéraud
with contributions from:
François Pottier
Armaël Guéneau
# -------------------------------------------------------------------------
# Private Makefile for package maintenance.
SHELL := bash
export CDPATH=
.PHONY: package export opam submit pin unpin
# -------------------------------------------------------------------------
include Makefile
# -------------------------------------------------------------------------
# Distribution.
# The version number is automatically set to the current date,
# unless DATE is defined on the command line.
DATE := $(shell /bin/date +%Y%m%d)
# The project name on gitlab.
PROJECT := cfml
# The opam package name.
PACKAGE := coq-$(PROJECT)
# The repository URL (https).
REPO := https://gitlab.inria.fr/charguer/$(PROJECT)
# The archive URL (https).
ARCHIVE := $(REPO)/repository/$(DATE)/archive.tar.gz
# The local repository directory.
PWD := $(shell pwd)
# -------------------------------------------------------------------------
# Prepare a release.
package:
# Make sure the correct version can be installed.
@ make reinstall
# -------------------------------------------------------------------------
# Publish a release. (Remember to commit everything first!)
export:
# Check if everything has been committed.
@ if [ -n "$$(git status --porcelain)" ] ; then \
echo "Error: there remain uncommitted changes." ; \
git status ; \
exit 1 ; \
else \
echo "Now making a release..." ; \
fi
# Create a git tag.
@ git tag -a $(DATE) -m "Release $(DATE)."
# Upload. (This automatically makes a .tar.gz archive available on gitlab.)
@ git push
@ git push --tags
# -------------------------------------------------------------------------
# Updating the opam package.
# This entry assumes that "make package" and "make export"
# have just been run (on the same day).
# You need opam-publish:
# sudo apt-get install libssl-dev
# opam install tls opam-publish
# In fact, you need a version of opam-publish that supports --subdirectory:
# git clone git@github.com:fpottier/opam-publish.git
# cd opam-publish
# git checkout 1.3
# opam pin add opam-publish `pwd` -k git
# The following command should have been run once:
# opam-publish repo add opam-coq-archive coq/opam-coq-archive
PUBLISH_OPTIONS := \
--repo opam-coq-archive \
--subdirectory released \
opam:
@ opam lint
@ opam-publish prepare $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE) $(ARCHIVE)
submit:
@ opam-publish submit $(PUBLISH_OPTIONS) $(PACKAGE).$(DATE)
# -------------------------------------------------------------------------
# Pinning.
pin:
opam pin add $(PACKAGE) `pwd` -k git
unpin:
opam pin remove $(PACKAGE)
MIT X11 LICENSE
---------------
Copyright (c) 2018 Arthur Charguéraud
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
Except as contained in this notice, the name of the copyright holders shall not
be used in advertising or otherwise to promote the sale, use or other dealings
in this Software without prior written authorization from the copyright holders.
\ No newline at end of file
...@@ -15,6 +15,9 @@ PREFIX ?= $(DEFAULT_PREFIX) ...@@ -15,6 +15,9 @@ PREFIX ?= $(DEFAULT_PREFIX)
BINDIR ?= $(PREFIX)/bin BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml LIBDIR ?= $(PREFIX)/lib/cfml
COQ_WHERE ?= $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
############################################################################## ##############################################################################
# Targets. # Targets.
...@@ -26,9 +29,7 @@ coqlib: ...@@ -26,9 +29,7 @@ coqlib:
generator: generator:
rm -f generator/cfml_config.ml rm -f generator/cfml_config.ml
sed -e 's|@@PREFIX@@|$(PREFIX)|' \ sed -e 's|@@LIBDIR@@|$(LIBDIR)|' \
-e 's|@@BINDIR@@|$(BINDIR)|' \
-e 's|@@LIBDIR@@|$(LIBDIR)|' \
generator/cfml_config.ml.in > generator/cfml_config.ml generator/cfml_config.ml.in > generator/cfml_config.ml
$(MAKE) -C generator $(MAKE) -C generator
...@@ -58,13 +59,6 @@ clean: ...@@ -58,13 +59,6 @@ clean:
############################################################################## ##############################################################################
# Installation. # Installation.
# If ARTHUR is defined, create a symbolic link from Coq's user-contrib
# directory to this directory (cfml). Otherwise, perform a copy.
# TEMPORARY, this is TODO
COQ_WHERE := $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
# As install depends on all, the file generator/cfml_config.ml is regenerated # As install depends on all, the file generator/cfml_config.ml is regenerated
# when `make install` is run; this ensures LIBDIR cannot be inconsistent. # when `make install` is run; this ensures LIBDIR cannot be inconsistent.
...@@ -102,7 +96,7 @@ uninstall: ...@@ -102,7 +96,7 @@ uninstall:
rm -f $(BINDIR)/cfmlc rm -f $(BINDIR)/cfmlc
# rm -f $(BINDIR)/cfml_cmj # rm -f $(BINDIR)/cfml_cmj
rm -rf $(LIBDIR) rm -rf $(LIBDIR)
rm -rf $(DOCDIR) # rm -rf $(DOCDIR)
rm -rf $(COQ_CONTRIB)/CFML rm -rf $(COQ_CONTRIB)/CFML
reinstall: uninstall reinstall: uninstall
......
# CFML : a characteristic formula generator for OCaml # CFML : a tool for proving OCaml programs in Separation Logic
Description Description
=========== ===========
CFML is a tool for carrying out proofs of correctness of OCaml programs with
respect to specifications expressed in higher-order Separation Logic.
CFML consists of two parts: CFML consists of two parts:
- a tool, implemented in OCaml, which parses OCaml source code
and generates Coq files containing characteristic formulae;
- a Coq library, which exports definitions, lemmas and tactics
used to manipulate characteristic formulae.
Status: - a tool, implemented in OCaml, parses OCaml source code and generates Coq
- The current version of CFML is known to work with Coq 8.6 files that contain characteristic formulae, that is, logical descriptions
of the behavior of the OCaml code.
- a Coq library exports definitions, lemmas, and tactics that are used
to reason inside Coq about the code. In short, these tactics allow
the reasoning rules of Separation Logic to be applied to the OCaml code.
Compilation Installation
============ ============
The recommended way is by using `opam` to pin the repository: The current version of CFML requires Coq 8.6 or newer.
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml The simplest way of installing the *latest released version* of CFML is via `opam`.
Note that you will need in particular a working installation ```sh
of [TLC](https://gitlab.inria.fr/charguer/tlc/). # This only needs to be done once, to add the opam repository with coq packages
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-cfml
```
If instead you wish to use *the development version* of CFML,
then the last line above should be replaced by the following:
```sh
opam pin add coq-cfml https://gitlab.inria.fr/charguer/cfml.git
```
Getting started Getting started
============ ============
...@@ -35,7 +50,7 @@ make ...@@ -35,7 +50,7 @@ make
coqide Tuto_proof.v coqide Tuto_proof.v
``` ```
- Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to setup a - Use [cfml-skeleton](https://gitlab.inria.fr/agueneau/cfml-skeleton) to set up a
new project that uses CFML. new project that uses CFML.
Documentation Documentation
......
Set Implicit Arguments. Set Implicit Arguments.
Require Export LibInt FuncDefs FuncPrint. Require Export LibInt FuncDefs FuncPrint.
Hint Resolve (0%nat) : typeclass_instances. Hint Resolve (0%nat) : typeclass_instances.
Hint Resolve (0%Z) : typeclass_instances. Hint Resolve (0%Z) : typeclass_instances.
......
...@@ -27,10 +27,10 @@ struct ...@@ -27,10 +27,10 @@ struct
let bucket h k = let bucket h k =
(H.hash k) mod (Array.length h) (H.hash k) mod (Array.length h)
let create n = let create n =
Array.create n [] Array.make n []
let rem h k = let rem h k =
let b = bucket h k in let b = bucket h k in
h.(b) <- List.filter (fun (k',_) -> not (H.equal k k')) h.(b) h.(b) <- List.filter (fun (k',_) -> not (H.equal k k')) h.(b)
...@@ -42,7 +42,7 @@ struct ...@@ -42,7 +42,7 @@ struct
let b = bucket h k in let b = bucket h k in
snd (List.find (fun (k',_) -> H.equal k k') h.(b)) snd (List.find (fun (k',_) -> H.equal k k') h.(b))
let add h k x = let add h k x =
if not (mem h k) then begin if not (mem h k) then begin
let b = bucket h k in let b = bucket h k in
h.(b) <- (k,x)::h.(b) h.(b) <- (k,x)::h.(b)
......
(** Representation of fixed-size circular buffers. *) (** Representation of fixed-size circular buffers. *)
module Make (Capa : CapacitySig.S) (Item : InhabType.S) = module Make (Capa : CapacitySig.S) (Item : InhabType.S) =
struct struct
(*--------------------------------------------------------------------------*) (*--------------------------------------------------------------------------*)
...@@ -24,7 +23,7 @@ type t = { ...@@ -24,7 +23,7 @@ type t = {
(** Builds a new queue *) (** Builds a new queue *)
let create () = let create () =
{ head = 0; { head = 0;
size = 0; size = 0;
data = Array.make capacity Item.inhab; } data = Array.make capacity Item.inhab; }
...@@ -59,15 +58,15 @@ let wrap_down i = ...@@ -59,15 +58,15 @@ let wrap_down i =
(** Pop an element from the front (assumes non-empty queue) *) (** Pop an element from the front (assumes non-empty queue) *)
let pop_front q = let pop_front q =
let x = Array.get q.data q.head in let x = Array.get q.data q.head in
q.head <- wrap_up (q.head + 1); q.head <- wrap_up (q.head + 1);
q.size <- q.size - 1; q.size <- q.size - 1;
x x
(** Pop an element from the back (assumes non-empty queue) *) (** Pop an element from the back (assumes non-empty queue) *)
let pop_back q = let pop_back q =
q.size <- q.size - 1; q.size <- q.size - 1;
let i = wrap_up (q.head + q.size) in let i = wrap_up (q.head + q.size) in
Array.get q.data i Array.get q.data i
...@@ -92,12 +91,12 @@ let push_back x q = ...@@ -92,12 +91,12 @@ let push_back x q =
let debug = false let debug = false
(** Internal: copy n elements from an array t1 of size capacity, (** Internal: copy n elements from an array t1 of size capacity,
starting at index i1 and possibly wrapping around, into an starting at index i1 and possibly wrapping around, into an
array t2 starting at index i2 and not wrapping around. *) array t2 starting at index i2 and not wrapping around. *)
let copy_data_wrap_src t1 i1 t2 i2 n = let copy_data_wrap_src t1 i1 t2 i2 n =
if (debug && (i1 < 0 || i1 > capacity || i2 < 0 || i2 + n > capacity || n < 0)) if (debug && (i1 < 0 || i1 > capacity || i2 < 0 || i2 + n > capacity || n < 0))
then failwith (Printf.sprintf "copy_data_wrap_src error: %d %d %d" i1 i2 n); then failwith (Printf.sprintf "copy_data_wrap_src error: %d %d %d" i1 i2 n);
let j1 = i1 + n in let j1 = i1 + n in
if j1 <= capacity then begin if j1 <= capacity then begin
Array.blit t1 i1 t2 i2 n Array.blit t1 i1 t2 i2 n
...@@ -107,7 +106,7 @@ let copy_data_wrap_src t1 i1 t2 i2 n = ...@@ -107,7 +106,7 @@ let copy_data_wrap_src t1 i1 t2 i2 n =
Array.blit t1 i1 t2 i2 na; Array.blit t1 i1 t2 i2 na;
Array.blit t1 0 t2 i2' (n - na); Array.blit t1 0 t2 i2' (n - na);
end end
(** Internal: copy n elements from an array t1 starting at index i1 (** Internal: copy n elements from an array t1 starting at index i1
and not wrapping around, into an array t2 of size capacity, and not wrapping around, into an array t2 of size capacity,
starting at index i2 and possibly wrapping around. *) starting at index i2 and possibly wrapping around. *)
...@@ -126,7 +125,7 @@ let copy_data_wrap_dst t1 i1 t2 i2 n = ...@@ -126,7 +125,7 @@ let copy_data_wrap_dst t1 i1 t2 i2 n =
end end
(** Internal: copy n elements from an array t1 starting at index i1 (** Internal: copy n elements from an array t1 starting at index i1
and possibly wrapping around, into an array t2 starting at index and possibly wrapping around, into an array t2 starting at index
i2 and possibly wrapping around. Both arrays are assumed to be i2 and possibly wrapping around. Both arrays are assumed to be
of size capacity. *) of size capacity. *)
...@@ -149,7 +148,7 @@ let copy_data_wrap_src_and_dst t1 i1 t2 i2 n = ...@@ -149,7 +148,7 @@ let copy_data_wrap_src_and_dst t1 i1 t2 i2 n =
(** Transfer N items from the back of a buffer to the front of another buffer *) (** Transfer N items from the back of a buffer to the front of another buffer *)
let transfer_back_to_front n q1 q2 = let transfer_back_to_front n q1 q2 =
if n < 0 || n > q1.size || n + q2.size > capacity if n < 0 || n > q1.size || n + q2.size > capacity
then invalid_arg "CircularArray.transfer_back_to_front"; then invalid_arg "CircularArray.transfer_back_to_front";
let h1 = wrap_down (wrap_up (q1.head + q1.size) - n) in let h1 = wrap_down (wrap_up (q1.head + q1.size) - n) in
let h2 = wrap_down (q2.head - n) in let h2 = wrap_down (q2.head - n) in
...@@ -161,7 +160,7 @@ let transfer_back_to_front n q1 q2 = ...@@ -161,7 +160,7 @@ let transfer_back_to_front n q1 q2 =
(** Transfer N items from the front of a buffer to the back of another buffer *) (** Transfer N items from the front of a buffer to the back of another buffer *)
let transfer_front_to_back n q1 q2 = let transfer_front_to_back n q1 q2 =
if n < 0 || n > q1.size || n + q2.size > capacity if n < 0 || n > q1.size || n + q2.size > capacity
then invalid_arg "CircularArray.transfer_front_to_back"; then invalid_arg "CircularArray.transfer_front_to_back";
let h1 = q1.head in let h1 = q1.head in
let h2 = wrap_up (q2.head + q2.size) in let h2 = wrap_up (q2.head + q2.size) in
...@@ -187,8 +186,8 @@ let transfer_all_to_back q1 q2 = ...@@ -187,8 +186,8 @@ let transfer_all_to_back q1 q2 =
(** Pop N elements from the front into an array *) (** Pop N elements from the front into an array *)
let popn_front_to_array n q = let popn_front_to_array n q =
if n < 0 || n > q.size if n < 0 || n > q.size
then invalid_arg "CircularArray.popn_front_to_array"; then invalid_arg "CircularArray.popn_front_to_array";
if n = 0 then [||] else begin if n = 0 then [||] else begin
let h = q.head in let h = q.head in
...@@ -201,7 +200,7 @@ let popn_front_to_array n q = ...@@ -201,7 +200,7 @@ let popn_front_to_array n q =
(** Pop N elements from the back into an array *) (** Pop N elements from the back into an array *)
let popn_back_to_array n q = let popn_back_to_array n q =
if n < 0 || n > q.size then invalid_arg "CircularArray.popn_back_to_array"; if n < 0 || n > q.size then invalid_arg "CircularArray.popn_back_to_array";
if n = 0 then [||] else begin if n = 0 then [||] else begin
let h = wrap_down (wrap_up (q.head + q.size) - n) in let h = wrap_down (wrap_up (q.head + q.size) - n) in
...@@ -281,7 +280,7 @@ let to_list q = ...@@ -281,7 +280,7 @@ let to_list q =
let cell_at q i = let cell_at q i =
wrap_up (q.head + i) wrap_up (q.head + i)
let get q i = let get q i =
q.data.(cell_at q i) q.data.(cell_at q i)
let set q i v = let set q i v =
......
(*************************************************************************) (*************************************************************************)
(** Graph representation by adjacency lists *) (** Graph representation by adjacency lists *)
module Graph = struct module Graph = struct
type t = (int list) array type t = (int list) array
let nb_nodes (g:t) = let nb_nodes (g:t) =
Array.length g Array.length g
let iter_edges (f:int->unit) (g:t) (i:int) = let iter_edges (g:t) (i:int) (f:int->unit) =
List.iter (fun j -> f j) g.(i) List.iter (fun j -> f j) g.(i)
end end
...@@ -28,15 +23,60 @@ type color = White | Gray | Black ...@@ -28,15 +23,60 @@ type color = White | Gray | Black
let rec dfs_from g c i = let rec dfs_from g c i =
c.(i) <- Gray; c.(i) <- Gray;
Graph.iter_edges (fun j -> Graph.iter_edges g i (fun j ->
if c.(j) = White if c.(j) = White
then dfs_from g c j) g i; then dfs_from g c j);
c.(i) <- Black c.(i) <- Black
let dfs_main g rs = let dfs_main g rs =
let n = Graph.nb_nodes g in let n = Graph.nb_nodes g in
let c = Array.make n White in let c = Array.make n White in
List.iter (fun i -> List.iter (fun i ->
if c.(i) = White then if c.(i) = White then
dfs_from g c i) rs; dfs_from g c i) rs;
c c
(*************************************************************************)
(** Minimal stack structure *)
module Stack = struct
type 'a t = ('a list) ref
let create () : 'a t =
ref []
let is_empty (s : 'a t) =
!s = []
let pop (s : 'a t) =
match !s with
| [] -> assert false
| x::n -> s := n; x
let push (x : 'a) (s : 'a t) =
s := x::!s
end
(*************************************************************************)
(** DFS Algorithm, using two colors and a stack *)
let reachable_imperative g a b =
let n = Graph.nb_nodes g in
let c = Array.make n false in
let s = Stack.create() in
c.(a) <- true;
Stack.push a s;
while not (Stack.is_empty s) do
let i = Stack.pop s in
Graph.iter_edges g i (fun j ->
if not c.(j) then begin
c.(j) <- true;
Stack.push j s;
end);
done;
c.(b)
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
open Pervasives open Pervasives
(** (**
* *
* This file contains unit tests for testing the generation of * This file contains unit tests for testing the generation of
* characteristic formulae, their display, and their associated * characteristic formulae, their display, and their associated
...@@ -8,13 +8,35 @@ open Pervasives ...@@ -8,13 +8,35 @@ open Pervasives
*) *)
(********************************************************************)
(* ** Ignored definitions *)
let ignored_def =
ignore "CFML";
3
let ignored_fun x =
ignore "CFML";
2 * x
let not_ignored_fun x =
ignore x;
2 * x
let rec ignored_fun2a x =
ignore "CFML";
ignored_fun2b x
and ignored_fun2b x =
ignored_fun2a x
(********************************************************************) (********************************************************************)
(* ** Notation for PRE/INV/POST *) (* ** Notation for PRE/INV/POST *)
let notation_inv_post r = let notation_inv_post r =
!r !r
let notation_pre_inv_post r s = let notation_pre_inv_post r s =
incr r; !s incr r; !s
...@@ -27,8 +49,8 @@ let notation_pre_inv_post r s = ...@@ -27,8 +49,8 @@ let notation_pre_inv_post r s =
type renaming_t' = int type renaming_t' = int
type renaming_t2 = C' type renaming_t2 = C'
type 'a renaming_t3 = int type 'a renaming_t3 = int
type 'a_ renaming_t4 = int type 'a_ renaming_t4 = int
let renaming_demo () = let renaming_demo () =
(* let x_ = 3 in --rejected *) (* let x_ = 3 in --rejected *)
...@@ -54,7 +76,7 @@ let let_poly_p1 () = ...@@ -54,7 +76,7 @@ let let_poly_p1 () =
let let_poly_p2 () = let let_poly_p2 () =
let f x = x in let f x = x in
let _r = let _r =
let _s = f None in () let _s = f None in ()
in in
() ()
...@@ -134,13 +156,13 @@ let let_poly_r2 () = ...@@ -134,13 +156,13 @@ let let_poly_r2 () =
y y
let let_poly_r3 () = let let_poly_r3 () =
let r = let r =
let x = ref [] in let x = ref [] in
[] in [] in
r r
(* ---Code not allowed because produces a ['_a list ref] at top level; (* ---Code not allowed because produces a ['_a list ref] at top level;
i.e. rejected when using OCaml "-strict_value_restriction" flag i.e. rejected when using OCaml "-strict_value_restriction" flag
let h1 = let h1 =
let f () : 'a list ref = ref [] in let f () : 'a list ref = ref [] in
f f
...@@ -149,7 +171,7 @@ let h1 = ...@@ -149,7 +171,7 @@ let h1 =
(********************************************************************) (********************************************************************)
(* ** Return *) (* ** Return *)
let ret_unit x = let ret_unit x =
() ()
...@@ -163,7 +185,7 @@ let ret_int_pair () = ...@@ -163,7 +185,7 @@ let ret_int_pair () =
let ret_poly () = let ret_poly () =
[] []
(* --Not yet supported: (* --Not yet supported:
Error is: Cannot infer this placeholder of type Type Error is: Cannot infer this placeholder of type Type
let ret_poly_internal () = let ret_poly_internal () =
let x = ignore None in let x = ignore None in
...@@ -173,7 +195,7 @@ let ret_poly_internal () = ...@@ -173,7 +195,7 @@ let ret_poly_internal () =
(* --TODO: BUG (* --TODO: BUG
The reference A_ was not found in the current environment.*) The reference A_ was not found in the current environment.*)
(* (*
let ret_poly_internal () = let ret_poly_internal () =
let x = ignore (None : 'a option) in let x = ignore (None : 'a option) in
() ()
...@@ -184,8 +206,8 @@ let ret_poly_internal () = ...@@ -184,8 +206,8 @@ let ret_poly_internal () =
(* ** Sequence *) (* ** Sequence *)
let seq_ret_unit () = let seq_ret_unit () =
ret_unit 1; ret_unit 1;
ret_unit 2; ret_unit 2;
ret_unit 3 ret_unit 3
...@@ -247,7 +269,7 @@ let let_fun_poly_pair_homogeneous () = ...@@ -247,7 +269,7 @@ let let_fun_poly_pair_homogeneous () =
f 3 3 f 3 3
let let_fun_on_the_fly () = let let_fun_on_the_fly () =
(fun x f -> f x) 3 (fun x -> x+1) (fun x f -> f x) 3 (fun x -> x+1)
let let_fun_in_let () = let let_fun_in_let () =
let f = (assert (true); fun x -> x) in let f = (assert (true); fun x -> x) in
...@@ -268,7 +290,7 @@ let app_partial_3_2 () = ...@@ -268,7 +290,7 @@ let app_partial_3_2 () =
let app_partial_add () = let app_partial_add () =
let add x y = x + y in let add x y = x + y in
let g = add 1 in g 2 let g = add 1 in g 2
let app_partial_appto () = let app_partial_appto () =
let appto x f = f x in let appto x f = f x in
let _r = appto 3 ((+) 1) in let _r = appto 3 ((+) 1) in
...@@ -301,7 +323,7 @@ let app_over_id () = ...@@ -301,7 +323,7 @@ let app_over_id () =
(********************************************************************) (********************************************************************)
(* ** Infix functions *) (* ** Infix functions *)
let (+++) x y = x + y let (+++) x y = x + y
let infix_aux x y = x +++ y let infix_aux x y = x +++ y
...@@ -336,7 +358,7 @@ let compare_min () = ...@@ -336,7 +358,7 @@ let compare_min () =
let compare_float () = let compare_float () =
(1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.) (1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.)
*) *)
let compare_poly () = let compare_poly () =
let _r1 = (None = None) in let _r1 = (None = None) in
let _r2 = (Some 3 = None) in let _r2 = (Some 3 = None) in
...@@ -347,8 +369,8 @@ let compare_poly () = ...@@ -347,8 +369,8 @@ let compare_poly () =
let f () = 4 in let f () = 4 in
let _r5 = ((Some f, None) = (None, Some f)) in *) let _r5 = ((Some f, None) = (None, Some f)) in *)
type 'a compare_poly_type = type 'a compare_poly_type =
| CompCst | CompCst
| CompPoly of 'a | CompPoly of 'a
| CompTuple of 'a * bool | CompTuple of 'a * bool
| CompFunc of ('a -> 'a) | CompFunc of ('a -> 'a)
...@@ -369,18 +391,18 @@ let compare_physical_loc_func () = ...@@ -369,18 +391,18 @@ let compare_physical_loc_func () =
let _r3 = if (f == f) then f() else 1 in let _r3 = if (f == f) then f() else 1 in
() ()
let compare_physical_algebraic () = let compare_physical_algebraic () =
let rec replace (k:int) (v:int) (l:(int*int) list) = let rec replace (k:int) (v:int) (l:(int*int) list) =
match l with match l with
| [] -> l | [] -> l
| (k2,v2)::t2 -> | (k2,v2)::t2 ->
let t = replace k v t2 in let t = replace k v t2 in
if k = k2 then (k,v)::t if k = k2 then (k,v)::t
else if t != t2 then (k2,v2)::t else if t != t2 then (k2,v2)::t
else l (* no change *) else l (* no change *)
in in
replace 1 9 [(1,3); (4,2); (2,5)] replace 1 9 [(1,3); (4,2); (2,5)]
(********************************************************************) (********************************************************************)
(* ** List operators *) (* ** List operators *)
...@@ -443,15 +465,15 @@ let (top_val_pair_fun_1,top_val_pair_fun_2) = ...@@ -443,15 +465,15 @@ let (top_val_pair_fun_1,top_val_pair_fun_2) =
(********************************************************************) (********************************************************************)
(* ** Polymorphic let bindings *) (* ** Polymorphic let bindings *)
let let_poly_nil () = let let_poly_nil () =
let x = [] in x let x = [] in x
let let_poly_nil_pair () = let let_poly_nil_pair () =
let x = ([], []) in x let x = ([], []) in x
let let_poly_nil_pair_homogeneous () = let let_poly_nil_pair_homogeneous () =
let x : ('a list * 'a list) = ([], []) in x let x : ('a list * 'a list) = ([], []) in x
let let_poly_nil_pair_heterogeneous () = let let_poly_nil_pair_heterogeneous () =
let x : ('a list * int list) = ([], []) in x let x : ('a list * int list) = ([], []) in x
...@@ -488,7 +510,7 @@ let match_nested () = ...@@ -488,7 +510,7 @@ let match_nested () =
(* TODO (* TODO
let match_term_when () = let match_term_when () =
let f x = x + 1 in let f x = x + 1 in
match f 3 with match f 3 with
| 0 -> 1 | 0 -> 1
| n when n > 0 -> 2 | n when n > 0 -> 2
| _ -> 3 | _ -> 3
...@@ -512,7 +534,7 @@ let exn_assert_false () = ...@@ -512,7 +534,7 @@ let exn_assert_false () =
let exn_failwith () = let exn_failwith () =
failwith "ok" failwith "ok"
exception My_exn exception My_exn
let exn_raise () = let exn_raise () =
raise My_exn raise My_exn
...@@ -522,7 +544,7 @@ let exn_raise () = ...@@ -522,7 +544,7 @@ let exn_raise () =
(* ** Assertions *) (* ** Assertions *)
let assert_true () = let assert_true () =
assert true; assert true;
3 3
let assert_pos x = let assert_pos x =
...@@ -530,16 +552,16 @@ let assert_pos x = ...@@ -530,16 +552,16 @@ let assert_pos x =
3 3
let assert_same (x:int) (y:int) = let assert_same (x:int) (y:int) =
assert (x = y); assert (x = y);
3 3
let assert_let () = let assert_let () =
assert (let _x = true in true); assert (let _x = true in true);
3 3
let assert_seq () = let assert_seq () =
let r = ref 0 in let r = ref 0 in
assert (incr r; true); assert (incr r; true);
!r !r
let assert_in_seq () = let assert_in_seq () =
...@@ -558,14 +580,14 @@ let if_term () = ...@@ -558,14 +580,14 @@ let if_term () =
let if_else_if () = let if_else_if () =
let f x = false in let f x = false in
if f 0 then 1 if f 0 then 1
else if f 1 then 2 else if f 1 then 2
else 0 else 0
let if_then_no_else b = let if_then_no_else b =
let r = ref 0 in let r = ref 0 in
if b if b
then incr r; then incr r;
!r !r
...@@ -584,10 +606,10 @@ let sitems_get_nb r = ...@@ -584,10 +606,10 @@ let sitems_get_nb r =
let sitems_incr_nb_let r = let sitems_incr_nb_let r =
let x = r.nb in let x = r.nb in
r.nb <- x + 1 r.nb <- x + 1
let sitems_incr_nb r = let sitems_incr_nb r =
r.nb <- r.nb + 1 r.nb <- r.nb + 1
let sitems_length_items_let r = let sitems_length_items_let r =
let x = r.items in let x = r.items in
...@@ -663,9 +685,9 @@ let ref_gc () = ...@@ -663,9 +685,9 @@ let ref_gc () =
let _r2 = ref 1 in let _r2 = ref 1 in
let _r3 = ref 1 in let _r3 = ref 1 in
let _r4 = ref 1 in let _r4 = ref 1 in
let x = let x =
let r5 = ref 2 in let r5 = ref 2 in
!r5 !r5
in in
x + !r1 x + !r1
...@@ -694,7 +716,7 @@ let array_ops () = ...@@ -694,7 +716,7 @@ let array_ops () =
let while_decr () = let while_decr () =
let n = ref 3 in let n = ref 3 in
let c = ref 0 in let c = ref 0 in
while !n > 0 do while !n > 0 do
incr c; incr c;
decr n; decr n;
done; done;
...@@ -766,14 +788,14 @@ type type_clashing_with_var = int ...@@ -766,14 +788,14 @@ type type_clashing_with_var = int
(********************************************************************) (********************************************************************)
(* ** Type algebraic *) (* ** Type algebraic *)
type 'a alga_three = type 'a alga_three =
| Alga_A | Alga_A
| Alga_B of int * int | Alga_B of int * int
| Alga_C of (int * int) | Alga_C of (int * int)
| Alga_D of 'a | Alga_D of 'a
| Alga_E of 'a * ('a -> 'a) | Alga_E of 'a * ('a -> 'a)
type ('a,'b) algb_erase = type ('a,'b) algb_erase =
| Algb_A of 'a | Algb_A of 'a
| Algb_B of (int -> 'b) | Algb_B of (int -> 'b)
...@@ -781,20 +803,33 @@ type ('a,'b) algb_erase = ...@@ -781,20 +803,33 @@ type ('a,'b) algb_erase =
(********************************************************************) (********************************************************************)
(* ** Type record *) (* ** Type record *)
type recorda = { type recorda = {
mutable recorda1 : int; mutable recorda1 : int;
mutable recorda2 : int } mutable recorda2 : int }
(*----*) (*----*)
type ('a,'b) recordb = type ('a,'b) recordb =
{ mutable recordb1 : 'a ; { mutable recordb1 : 'a ;
mutable recordb2 : 'b -> 'b } mutable recordb2 : 'b -> 'b }
(* not supported: record overloading of fields (* not supported: record overloading of fields
-- else would need to prefix all fields with the type... *) -- else would need to prefix all fields with the type... *)
(********************************************************************)
(* ** Recursive definitions are supported for heap-allocated records *)
type 'a node = {
mutable data : 'a;
mutable prev : 'a node;
mutable next : 'a node;
}
let create_cyclic_node (data: 'a): 'a node =
let rec node = { data; prev = node; next = node } in
node
(********************************************************************) (********************************************************************)
(* ** Type mutual *) (* ** Type mutual *)
...@@ -832,14 +867,14 @@ type typerecb1 = | Typerecb_1 of typerecb1 typerecb2 ...@@ -832,14 +867,14 @@ type typerecb1 = | Typerecb_1 of typerecb1 typerecb2
(*----*) (*----*)
(* Circularity between mutable records and inductive is broken (* Circularity between mutable records and inductive is broken
through the indirection at type loc *) through the indirection at type loc *)
type 'a typerecd1 = { mutable typerecd1_f : 'a typerecd2 } type 'a typerecd1 = { mutable typerecd1_f : 'a typerecd2 }
and 'a typerecd2 = and 'a typerecd2 =
| Typerecd_2a | Typerecd_2a
| Typerecd_2b of 'a typerecd1 | Typerecd_2b of 'a typerecd1
| Typerecd_2c of 'a typerecd3 | Typerecd_2c of 'a typerecd3
and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 } and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }
...@@ -848,7 +883,7 @@ and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 } ...@@ -848,7 +883,7 @@ and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }
(* ** Local module *) (* ** Local module *)
module ModFoo = struct module ModFoo = struct
type t = int type t = int
let x : t = 3 let x : t = 3
...@@ -866,7 +901,7 @@ module type ModBarType = sig ...@@ -866,7 +901,7 @@ module type ModBarType = sig
end end
module ModBar : ModBarType = struct module ModBar : ModBarType = struct
type t = int type t = int
let x : t = 3 let x : t = 3
...@@ -877,14 +912,14 @@ end ...@@ -877,14 +912,14 @@ end
(* ** Functor *) (* ** Functor *)
module ModFunctor (Bar : ModBarType) = struct module ModFunctor (Bar : ModBarType) = struct
type u = Bar.t type u = Bar.t
let x : u = Bar.x let x : u = Bar.x
end end
module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct
type t = Bar.t type t = Bar.t
let x : t = Bar.x let x : t = Bar.x
...@@ -936,7 +971,7 @@ let list_ops () = ...@@ -936,7 +971,7 @@ let list_ops () =
(* TODO (* TODO
let match_term_when () = let match_term_when () =
let f x = x + 1 in let f x = x + 1 in
match f 3 with match f 3 with
| 0 -> 1 | 0 -> 1
| n when n > 0 -> 2 | n when n > 0 -> 2
| _ -> 3 | _ -> 3
......
...@@ -2,6 +2,7 @@ Set Implicit Arguments. ...@@ -2,6 +2,7 @@ Set Implicit Arguments.
Require Import CFML.CFLib. Require Import CFML.CFLib.
Require Import Demo_ml. Require Import Demo_ml.
Require Import Stdlib. Require Import Stdlib.
Require TLC.LibListZ.
Import ZsubNoSimpl. Import ZsubNoSimpl.
Open Scope tag_scope. Open Scope tag_scope.
...@@ -378,7 +379,7 @@ Proof using. ...@@ -378,7 +379,7 @@ Proof using.
xapp2. xapp2.
dup 5. dup 5.
{ apply Spec. xrets. auto. } { apply Spec. xrets. auto. }
{ xapp3_no_apply. Focus 2. apply S. xrets. auto. } { xapp3_no_apply. 2:{ apply S. } xrets. auto. }
{ xapp3_no_simpl. xrets~. skip. skip. } { xapp3_no_simpl. xrets~. skip. skip. }
{ xapp3. xrets~. } { xapp3. xrets~. }
{ xapp. xret. xsimpl~. } } { xapp. xret. xsimpl~. } }
...@@ -1353,6 +1354,15 @@ Qed. ...@@ -1353,6 +1354,15 @@ Qed.
Definition Sitems A (L:list A) r := Definition Sitems A (L:list A) r :=
Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ]. Hexists n, r ~> `{ nb' := n; items' := L } \* \[ n = LibListZ.length L ].
(********************************************************************)
(* ** Recursive records definitions *)
Lemma create_cyclic_node_spec : forall (A:Type) (data:A),
app create_cyclic_node [data]
PRE \[]
POST (fun (r: loc) => r ~> `{ data' := data; prev' := r; next' := r }).
Proof using. xcf_go~. Qed.
(* (*
Section ProjLemma. Section ProjLemma.
Variables (B:Type) (A1 : Type). Variables (B:Type) (A1 : Type).
...@@ -1417,7 +1427,16 @@ Proof using. ...@@ -1417,7 +1427,16 @@ Proof using.
xcf. dup 2. xcf. dup 2.
{ xopen r. xpull ;=> n E. skip. } { xopen r. xpull ;=> n E. skip. }
{ xopenx r ;=> n E. xapps. xapps. xapps. xapp. { xopenx r ;=> n E. xapps. xapps. xapps. xapp.
xclose r. rew_list; math. xsimpl~. } intros v.
dup 4.
{ (* details *)
xclose_show_core r. xchange H. skip. skip. (* demo *) }
{ (* with explicit arguments, incorrect instantiation *)
xclose (>> r L n). auto. skip. skip. (* demo *) }
{ (* with explicit arguments, correct instantiation *)
xclose (>> r (x::L) (n+1)). rew_list; math. xsimpl~. }
{ (* short form *)
xclose r. rew_list; math. xsimpl~. } }
Qed. Qed.
......
This diff is collapsed.
This diff is collapsed.
...@@ -94,13 +94,13 @@ type t_compact = ...@@ -94,13 +94,13 @@ type t_compact =
mutable c_last_used : int ; } mutable c_last_used : int ; }
let create_compact () = let create_compact () =
{ c_trans = Array.create 1024 0 ; { c_trans = Array.make 1024 0 ;
c_check = Array.create 1024 (-1) ; c_check = Array.make 1024 (-1) ;
c_last_used = 0 ; } c_last_used = 0 ; }
let reset_compact c = let reset_compact c =
c.c_trans <- Array.create 1024 0 ; c.c_trans <- Array.make 1024 0 ;
c.c_check <- Array.create 1024 (-1) ; c.c_check <- Array.make 1024 (-1) ;
c.c_last_used <- 0 c.c_last_used <- 0
(* One compacted table for transitions, one other for memory actions *) (* One compacted table for transitions, one other for memory actions *)
...@@ -112,9 +112,9 @@ let grow_compact c = ...@@ -112,9 +112,9 @@ let grow_compact c =
let old_trans = c.c_trans let old_trans = c.c_trans
and old_check = c.c_check in and old_check = c.c_check in
let n = Array.length old_trans in let n = Array.length old_trans in
c.c_trans <- Array.create (2*n) 0; c.c_trans <- Array.make (2*n) 0;
Array.blit old_trans 0 c.c_trans 0 c.c_last_used; Array.blit old_trans 0 c.c_trans 0 c.c_last_used;
c.c_check <- Array.create (2*n) (-1); c.c_check <- Array.make (2*n) (-1);
Array.blit old_check 0 c.c_check 0 c.c_last_used Array.blit old_check 0 c.c_check 0 c.c_last_used
let do_pack state_num orig compact = let do_pack state_num orig compact =
...@@ -144,8 +144,8 @@ let do_pack state_num orig compact = ...@@ -144,8 +144,8 @@ let do_pack state_num orig compact =
(base, default) (base, default)
let pack_moves state_num move_t = let pack_moves state_num move_t =
let move_v = Array.create 257 0 let move_v = Array.make 257 0
and move_m = Array.create 257 0 in and move_m = Array.make 257 0 in
for i = 0 to 256 do for i = 0 to 256 do
let act,c = move_t.(i) in let act,c = move_t.(i) in
move_v.(i) <- (match act with Backtrack -> -1 | Goto n -> n) ; move_v.(i) <- (match act with Backtrack -> -1 | Goto n -> n) ;
...@@ -177,12 +177,12 @@ type lex_tables = ...@@ -177,12 +177,12 @@ type lex_tables =
let compact_tables state_v = let compact_tables state_v =
let n = Array.length state_v in let n = Array.length state_v in
let base = Array.create n 0 let base = Array.make n 0
and backtrk = Array.create n (-1) and backtrk = Array.make n (-1)
and default = Array.create n 0 and default = Array.make n 0
and base_code = Array.create n 0 and base_code = Array.make n 0
and backtrk_code = Array.create n 0 and backtrk_code = Array.make n 0
and default_code = Array.create n 0 in and default_code = Array.make n 0 in
for i = 0 to n - 1 do for i = 0 to n - 1 do
match state_v.(i) with match state_v.(i) with
| Perform (n,c) -> | Perform (n,c) ->
......
...@@ -84,7 +84,7 @@ let complement s = diff all_chars s ...@@ -84,7 +84,7 @@ let complement s = diff all_chars s
let env_to_array env = match env with let env_to_array env = match env with
| [] -> assert false | [] -> assert false
| (_,x)::rem -> | (_,x)::rem ->
let res = Array.create 257 x in let res = Array.make 257 x in
List.iter List.iter
(fun (c,y) -> (fun (c,y) ->
List.iter List.iter
......
...@@ -590,7 +590,7 @@ let rec firstpos = function ...@@ -590,7 +590,7 @@ let rec firstpos = function
(* Berry-sethi followpos *) (* Berry-sethi followpos *)
let followpos size entry_list = let followpos size entry_list =
let v = Array.create size TransSet.empty in let v = Array.make size TransSet.empty in
let rec fill s = function let rec fill s = function
| Empty|Action _|Tag _ -> () | Empty|Action _|Tag _ -> ()
| Chars (n,_) -> v.(n) <- s | Chars (n,_) -> v.(n) <- s
...@@ -1131,7 +1131,7 @@ let make_tag_entry id start act a r = match a with ...@@ -1131,7 +1131,7 @@ let make_tag_entry id start act a r = match a with
| _ -> r | _ -> r
let extract_tags l = let extract_tags l =
let envs = Array.create (List.length l) TagMap.empty in let envs = Array.make (List.length l) TagMap.empty in
List.iter List.iter
(fun (act,m,_) -> (fun (act,m,_) ->
envs.(act) <- envs.(act) <-
...@@ -1185,7 +1185,7 @@ let make_dfa lexdef = ...@@ -1185,7 +1185,7 @@ let make_dfa lexdef =
done ; done ;
eprintf "%d states\n" !next_state_num ; eprintf "%d states\n" !next_state_num ;
*) *)
let actions = Array.create !next_state_num (Perform (0,[])) in let actions = Array.make !next_state_num (Perform (0,[])) in
List.iter (fun (act, i) -> actions.(i) <- act) states; List.iter (fun (act, i) -> actions.(i) <- act) states;
(* Useless state reset, so as to restrict GC roots *) (* Useless state reset, so as to restrict GC roots *)
reset_state () ; reset_state () ;
......
...@@ -80,7 +80,7 @@ let output_entry sourcefile ic oc oci e = ...@@ -80,7 +80,7 @@ let output_entry sourcefile ic oc oci e =
output_args e.auto_args output_args e.auto_args
(fun oc x -> (fun oc x ->
if x > 0 then if x > 0 then
fprintf oc "lexbuf.Lexing.lex_mem <- Array.create %d (-1) ; " x) fprintf oc "lexbuf.Lexing.lex_mem <- Array.make %d (-1) ; " x)
e.auto_mem_size e.auto_mem_size
(output_memory_actions " ") init_moves (output_memory_actions " ") init_moves
e.auto_name e.auto_name
......
...@@ -22,7 +22,7 @@ open Common ...@@ -22,7 +22,7 @@ open Common
let output_auto_defs oc = let output_auto_defs oc =
fprintf oc "let __ocaml_lex_init_lexbuf lexbuf mem_size =\n\ fprintf oc "let __ocaml_lex_init_lexbuf lexbuf mem_size =\n\
let pos = lexbuf.Lexing.lex_curr_pos in\n\ let pos = lexbuf.Lexing.lex_curr_pos in\n\
lexbuf.Lexing.lex_mem <- Array.create mem_size (-1) ;\n\ lexbuf.Lexing.lex_mem <- Array.make mem_size (-1) ;\n\
lexbuf.Lexing.lex_start_pos <- pos ;\n\ lexbuf.Lexing.lex_start_pos <- pos ;\n\
lexbuf.Lexing.lex_last_pos <- pos ;\n\ lexbuf.Lexing.lex_last_pos <- pos ;\n\
lexbuf.Lexing.lex_last_action <- -1\n\ lexbuf.Lexing.lex_last_action <- -1\n\
......
...@@ -15,12 +15,12 @@ type 'a t = {mutable next : int ; mutable data : 'a array} ...@@ -15,12 +15,12 @@ type 'a t = {mutable next : int ; mutable data : 'a array}
let default_size = 32 let default_size = 32
;; ;;
let create x = {next = 0 ; data = Array.create default_size x} let create x = {next = 0 ; data = Array.make default_size x}
and reset t = t.next <- 0 and reset t = t.next <- 0
;; ;;
let incr_table table new_size = let incr_table table new_size =
let t = Array.create new_size table.data.(0) in let t = Array.make new_size table.data.(0) in
Array.blit table.data 0 t 0 (Array.length table.data) ; Array.blit table.data 0 t 0 (Array.length table.data) ;
table.data <- t table.data <- t
......
...@@ -91,12 +91,12 @@ let _ = ...@@ -91,12 +91,12 @@ let _ =
let outputfile : string = let outputfile : string =
match !outputfile with match !outputfile with
| None -> | None ->
Filename.concat dirname ((String.capitalize basename) ^ "_ml.v") Filename.concat dirname ((String.capitalize_ascii basename) ^ "_ml.v")
| Some f -> | Some f ->
f f
in in
let debugdir = Filename.concat dirname "_output" in let debugdir = Filename.concat dirname "_output" in
let debugdirBase = Filename.concat debugdir (String.capitalize basename) in let debugdirBase = Filename.concat debugdir (String.capitalize_ascii basename) in
(* FAILURE ON WINDOWS *) (* FAILURE ON WINDOWS *)
let cmd = Printf.sprintf "mkdir -p %s" debugdir in let cmd = Printf.sprintf "mkdir -p %s" debugdir in
begin try ignore (Sys.command cmd) begin try ignore (Sys.command cmd)
......
...@@ -131,27 +131,20 @@ let str_cmp (s1:string) (s2:string) = ...@@ -131,27 +131,20 @@ let str_cmp (s1:string) (s2:string) =
let str_starts_with p s = let str_starts_with p s =
let n = String.length p in let n = String.length p in
String.length s >= n String.length s >= n
&& String.sub s 0 n = p && String.sub s 0 n = p
let str_replace char1 char2 s =
let s2 = String.copy s in
for i = 0 to pred (String.length s) do
if s2.[i] = char1 then s2.[i] <- char2;
done;
s2
let str_capitalize_1 s = let str_capitalize_1 s =
if String.length s <= 0 then s else if String.length s <= 0 then s else
let s' = String.copy s in let s' = Bytes.of_string s in
s'.[0] <- Char.uppercase s.[0]; Bytes.set s' 0 (Char.uppercase s.[0]);
s' Bytes.unsafe_to_string s'
let str_capitalize_2 s = let str_capitalize_2 s =
if String.length s < 2 then s else if String.length s < 2 then s else
let s' = String.copy s in let s' = Bytes.of_string s in
s'.[1] <- Char.uppercase s.[1]; Bytes.set s' 1 (Char.uppercase s.[1]);
s' Bytes.unsafe_to_string s'
(**************************************************************) (**************************************************************)
......
...@@ -53,7 +53,6 @@ val list_index : 'a -> 'a list -> int ...@@ -53,7 +53,6 @@ val list_index : 'a -> 'a list -> int
val str_cmp : string -> string -> int val str_cmp : string -> string -> int
val str_starts_with : string -> string -> bool val str_starts_with : string -> string -> bool
val str_replace : char -> char -> string -> string
(** Capitalize the first letter of a string (if any) *) (** Capitalize the first letter of a string (if any) *)
......