...
 
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)
BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml
COQ_WHERE ?= $(shell $(COQBIN)coqc -where)
COQ_CONTRIB := $(COQ_WHERE)/user-contrib
##############################################################################
# Targets.
......@@ -26,9 +29,7 @@ coqlib:
generator:
rm -f generator/cfml_config.ml
sed -e 's|@@PREFIX@@|$(PREFIX)|' \
-e 's|@@BINDIR@@|$(BINDIR)|' \
-e 's|@@LIBDIR@@|$(LIBDIR)|' \
sed -e 's|@@LIBDIR@@|$(LIBDIR)|' \
generator/cfml_config.ml.in > generator/cfml_config.ml
$(MAKE) -C generator
......@@ -58,13 +59,6 @@ clean:
##############################################################################
# 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
# when `make install` is run; this ensures LIBDIR cannot be inconsistent.
......@@ -102,7 +96,7 @@ uninstall:
rm -f $(BINDIR)/cfmlc
# rm -f $(BINDIR)/cfml_cmj
rm -rf $(LIBDIR)
rm -rf $(DOCDIR)
# rm -rf $(DOCDIR)
rm -rf $(COQ_CONTRIB)/CFML
reinstall: uninstall
......
# CFML : a characteristic formula generator for OCaml
# CFML : a tool for proving OCaml programs in Separation Logic
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:
- 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:
- The current version of CFML is known to work with Coq 8.6
- a tool, implemented in OCaml, parses OCaml source code and generates Coq
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
of [TLC](https://gitlab.inria.fr/charguer/tlc/).
```sh
# 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
============
......@@ -35,7 +50,7 @@ make
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.
Documentation
......
Set Implicit Arguments.
Require Export LibInt FuncDefs FuncPrint.
Require Export LibInt FuncDefs FuncPrint.
Hint Resolve (0%nat) : typeclass_instances.
Hint Resolve (0%Z) : typeclass_instances.
......
......@@ -27,10 +27,10 @@ struct
let bucket h k =
(H.hash k) mod (Array.length h)
let create n =
Array.create n []
let create n =
Array.make n []
let rem h k =
let rem h k =
let b = bucket h k in
h.(b) <- List.filter (fun (k',_) -> not (H.equal k k')) h.(b)
......@@ -42,7 +42,7 @@ struct
let b = bucket h k in
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
let b = bucket h k in
h.(b) <- (k,x)::h.(b)
......
(** Representation of fixed-size circular buffers. *)
module Make (Capa : CapacitySig.S) (Item : InhabType.S) =
module Make (Capa : CapacitySig.S) (Item : InhabType.S) =
struct
(*--------------------------------------------------------------------------*)
......@@ -24,7 +23,7 @@ type t = {
(** Builds a new queue *)
let create () =
let create () =
{ head = 0;
size = 0;
data = Array.make capacity Item.inhab; }
......@@ -59,15 +58,15 @@ let wrap_down i =
(** 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
q.head <- wrap_up (q.head + 1);
q.size <- q.size - 1;
x
(** Pop an element from the back (assumes non-empty queue) *)
let pop_back q =
let pop_back q =
q.size <- q.size - 1;
let i = wrap_up (q.head + q.size) in
Array.get q.data i
......@@ -92,12 +91,12 @@ let push_back x q =
let debug = false
(** 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. *)
let copy_data_wrap_src t1 i1 t2 i2 n =
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
if j1 <= capacity then begin
Array.blit 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 0 t2 i2' (n - na);
end
(** Internal: copy n elements from an array t1 starting at index i1
and not wrapping around, into an array t2 of size capacity,
starting at index i2 and possibly wrapping around. *)
......@@ -126,7 +125,7 @@ let copy_data_wrap_dst t1 i1 t2 i2 n =
end
(** 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
of size capacity. *)
......@@ -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 *)
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";
let h1 = wrap_down (wrap_up (q1.head + q1.size) - n) in
let h2 = wrap_down (q2.head - n) in
......@@ -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 *)
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";
let h1 = q1.head in
let h2 = wrap_up (q2.head + q2.size) in
......@@ -187,8 +186,8 @@ let transfer_all_to_back q1 q2 =
(** Pop N elements from the front into an array *)
let popn_front_to_array n q =
if n < 0 || n > q.size
let popn_front_to_array n q =
if n < 0 || n > q.size
then invalid_arg "CircularArray.popn_front_to_array";
if n = 0 then [||] else begin
let h = q.head in
......@@ -201,7 +200,7 @@ let popn_front_to_array n q =
(** 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 then [||] else begin
let h = wrap_down (wrap_up (q.head + q.size) - n) in
......@@ -281,7 +280,7 @@ let to_list q =
let cell_at q i =
wrap_up (q.head + i)
let get q i =
let get q i =
q.data.(cell_at q i)
let set q i v =
......
(*************************************************************************)
(** Graph representation by adjacency lists *)
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
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)
end
......@@ -28,15 +23,60 @@ type color = White | Gray | Black
let rec dfs_from g c i =
c.(i) <- Gray;
Graph.iter_edges (fun j ->
if c.(j) = White
then dfs_from g c j) g i;
Graph.iter_edges g i (fun j ->
if c.(j) = White
then dfs_from g c j);
c.(i) <- Black
let dfs_main g rs =
let n = Graph.nb_nodes g in
let c = Array.make n White in
List.iter (fun i ->
List.iter (fun i ->
if c.(i) = White then
dfs_from g c i) rs;
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
(**
(**
*
* This file contains unit tests for testing the generation of
* characteristic formulae, their display, and their associated
......@@ -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 *)
let notation_inv_post r =
let notation_inv_post r =
!r
let notation_pre_inv_post r s =
let notation_pre_inv_post r s =
incr r; !s
......@@ -27,8 +49,8 @@ let notation_pre_inv_post r s =
type renaming_t' = int
type renaming_t2 = C'
type 'a renaming_t3 = int
type 'a_ renaming_t4 = int
type 'a renaming_t3 = int
type 'a_ renaming_t4 = int
let renaming_demo () =
(* let x_ = 3 in --rejected *)
......@@ -54,7 +76,7 @@ let let_poly_p1 () =
let let_poly_p2 () =
let f x = x in
let _r =
let _r =
let _s = f None in ()
in
()
......@@ -134,13 +156,13 @@ let let_poly_r2 () =
y
let let_poly_r3 () =
let r =
let r =
let x = ref [] in
[] in
r
(* ---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 f () : 'a list ref = ref [] in
f
......@@ -149,7 +171,7 @@ let h1 =
(********************************************************************)
(* ** Return *)
(* ** Return *)
let ret_unit x =
()
......@@ -163,7 +185,7 @@ let ret_int_pair () =
let ret_poly () =
[]
(* --Not yet supported:
(* --Not yet supported:
Error is: Cannot infer this placeholder of type Type
let ret_poly_internal () =
let x = ignore None in
......@@ -173,7 +195,7 @@ let ret_poly_internal () =
(* --TODO: BUG
The reference A_ was not found in the current environment.*)
(*
(*
let ret_poly_internal () =
let x = ignore (None : 'a option) in
()
......@@ -184,8 +206,8 @@ let ret_poly_internal () =
(* ** Sequence *)
let seq_ret_unit () =
ret_unit 1;
ret_unit 2;
ret_unit 1;
ret_unit 2;
ret_unit 3
......@@ -247,7 +269,7 @@ let let_fun_poly_pair_homogeneous () =
f 3 3
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 f = (assert (true); fun x -> x) in
......@@ -268,7 +290,7 @@ let app_partial_3_2 () =
let app_partial_add () =
let add x y = x + y in
let g = add 1 in g 2
let app_partial_appto () =
let appto x f = f x in
let _r = appto 3 ((+) 1) in
......@@ -301,7 +323,7 @@ let app_over_id () =
(********************************************************************)
(* ** Infix functions *)
let (+++) x y = x + y
let (+++) x y = x + y
let infix_aux x y = x +++ y
......@@ -336,7 +358,7 @@ let compare_min () =
let compare_float () =
(1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.)
*)
let compare_poly () =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
......@@ -347,8 +369,8 @@ let compare_poly () =
let f () = 4 in
let _r5 = ((Some f, None) = (None, Some f)) in *)
type 'a compare_poly_type =
| CompCst
type 'a compare_poly_type =
| CompCst
| CompPoly of 'a
| CompTuple of 'a * bool
| CompFunc of ('a -> 'a)
......@@ -369,18 +391,18 @@ let compare_physical_loc_func () =
let _r3 = if (f == f) then f() else 1 in
()
let compare_physical_algebraic () =
let rec replace (k:int) (v:int) (l:(int*int) list) =
let compare_physical_algebraic () =
let rec replace (k:int) (v:int) (l:(int*int) list) =
match l with
| [] -> l
| (k2,v2)::t2 ->
| (k2,v2)::t2 ->
let t = replace k v t2 in
if k = k2 then (k,v)::t
else if t != t2 then (k2,v2)::t
else l (* no change *)
in
replace 1 9 [(1,3); (4,2); (2,5)]
replace 1 9 [(1,3); (4,2); (2,5)]
(********************************************************************)
(* ** List operators *)
......@@ -443,15 +465,15 @@ let (top_val_pair_fun_1,top_val_pair_fun_2) =
(********************************************************************)
(* ** Polymorphic let bindings *)
let let_poly_nil () =
let let_poly_nil () =
let x = [] in x
let let_poly_nil_pair () =
let let_poly_nil_pair () =
let x = ([], []) in x
let let_poly_nil_pair_homogeneous () =
let x : ('a list * 'a list) = ([], []) in x
let let_poly_nil_pair_heterogeneous () =
let x : ('a list * int list) = ([], []) in x
......@@ -488,7 +510,7 @@ let match_nested () =
(* TODO
let match_term_when () =
let f x = x + 1 in
match f 3 with
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
......@@ -512,7 +534,7 @@ let exn_assert_false () =
let exn_failwith () =
failwith "ok"
exception My_exn
exception My_exn
let exn_raise () =
raise My_exn
......@@ -522,7 +544,7 @@ let exn_raise () =
(* ** Assertions *)
let assert_true () =
assert true;
assert true;
3
let assert_pos x =
......@@ -530,16 +552,16 @@ let assert_pos x =
3
let assert_same (x:int) (y:int) =
assert (x = y);
assert (x = y);
3
let assert_let () =
assert (let _x = true in true);
assert (let _x = true in true);
3
let assert_seq () =
let r = ref 0 in
assert (incr r; true);
assert (incr r; true);
!r
let assert_in_seq () =
......@@ -558,14 +580,14 @@ let if_term () =
let if_else_if () =
let f x = false in
if f 0 then 1
if f 0 then 1
else if f 1 then 2
else 0
let if_then_no_else b =
let r = ref 0 in
if b
then incr r;
then incr r;
!r
......@@ -584,10 +606,10 @@ let sitems_get_nb r =
let sitems_incr_nb_let r =
let x = r.nb in
r.nb <- x + 1
r.nb <- x + 1
let sitems_incr_nb r =
r.nb <- r.nb + 1
r.nb <- r.nb + 1
let sitems_length_items_let r =
let x = r.items in
......@@ -663,9 +685,9 @@ let ref_gc () =
let _r2 = ref 1 in
let _r3 = ref 1 in
let _r4 = ref 1 in
let x =
let x =
let r5 = ref 2 in
!r5
!r5
in
x + !r1
......@@ -694,7 +716,7 @@ let array_ops () =
let while_decr () =
let n = ref 3 in
let c = ref 0 in
while !n > 0 do
while !n > 0 do
incr c;
decr n;
done;
......@@ -766,14 +788,14 @@ type type_clashing_with_var = int
(********************************************************************)
(* ** Type algebraic *)
type 'a alga_three =
| Alga_A
| Alga_B of int * int
type 'a alga_three =
| Alga_A
| Alga_B of int * int
| Alga_C of (int * int)
| Alga_D of 'a
| Alga_D of 'a
| Alga_E of 'a * ('a -> 'a)
type ('a,'b) algb_erase =
type ('a,'b) algb_erase =
| Algb_A of 'a
| Algb_B of (int -> 'b)
......@@ -781,20 +803,33 @@ type ('a,'b) algb_erase =
(********************************************************************)
(* ** Type record *)
type recorda = {
mutable recorda1 : int;
type recorda = {
mutable recorda1 : int;
mutable recorda2 : int }
(*----*)
type ('a,'b) recordb =
{ mutable recordb1 : 'a ;
type ('a,'b) recordb =
{ mutable recordb1 : 'a ;
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... *)
(********************************************************************)
(* ** 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 *)
......@@ -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 *)
type 'a typerecd1 = { mutable typerecd1_f : 'a typerecd2 }
and 'a typerecd2 =
| Typerecd_2a
| Typerecd_2b of 'a typerecd1
| Typerecd_2c of 'a typerecd3
and 'a typerecd2 =
| Typerecd_2a
| Typerecd_2b of 'a typerecd1
| Typerecd_2c of 'a typerecd3
and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }
......@@ -848,7 +883,7 @@ and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }
(* ** Local module *)
module ModFoo = struct
type t = int
let x : t = 3
......@@ -866,7 +901,7 @@ module type ModBarType = sig
end
module ModBar : ModBarType = struct
type t = int
let x : t = 3
......@@ -877,14 +912,14 @@ end
(* ** Functor *)
module ModFunctor (Bar : ModBarType) = struct
type u = Bar.t
let x : u = Bar.x
end
module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct
type t = Bar.t
let x : t = Bar.x
......@@ -936,7 +971,7 @@ let list_ops () =
(* TODO
let match_term_when () =
let f x = x + 1 in
match f 3 with
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
......
......@@ -2,6 +2,7 @@ Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Require TLC.LibListZ.
Import ZsubNoSimpl.
Open Scope tag_scope.
......@@ -378,7 +379,7 @@ Proof using.
xapp2.
dup 5.
{ 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. xrets~. }
{ xapp. xret. xsimpl~. } }
......@@ -1353,6 +1354,15 @@ Qed.
Definition Sitems A (L:list A) r :=
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.
Variables (B:Type) (A1 : Type).
......@@ -1417,7 +1427,16 @@ Proof using.
xcf. dup 2.
{ xopen r. xpull ;=> n E. skip. }
{ 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.
......
This diff is collapsed.
This diff is collapsed.
......@@ -94,13 +94,13 @@ type t_compact =
mutable c_last_used : int ; }
let create_compact () =
{ c_trans = Array.create 1024 0 ;
c_check = Array.create 1024 (-1) ;
{ c_trans = Array.make 1024 0 ;
c_check = Array.make 1024 (-1) ;
c_last_used = 0 ; }
let reset_compact c =
c.c_trans <- Array.create 1024 0 ;
c.c_check <- Array.create 1024 (-1) ;
c.c_trans <- Array.make 1024 0 ;
c.c_check <- Array.make 1024 (-1) ;
c.c_last_used <- 0
(* One compacted table for transitions, one other for memory actions *)
......@@ -112,9 +112,9 @@ let grow_compact c =
let old_trans = c.c_trans
and old_check = c.c_check 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;
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
let do_pack state_num orig compact =
......@@ -144,8 +144,8 @@ let do_pack state_num orig compact =
(base, default)
let pack_moves state_num move_t =
let move_v = Array.create 257 0
and move_m = Array.create 257 0 in
let move_v = Array.make 257 0
and move_m = Array.make 257 0 in
for i = 0 to 256 do
let act,c = move_t.(i) in
move_v.(i) <- (match act with Backtrack -> -1 | Goto n -> n) ;
......@@ -177,12 +177,12 @@ type lex_tables =
let compact_tables state_v =
let n = Array.length state_v in
let base = Array.create n 0
and backtrk = Array.create n (-1)
and default = Array.create n 0
and base_code = Array.create n 0
and backtrk_code = Array.create n 0
and default_code = Array.create n 0 in
let base = Array.make n 0
and backtrk = Array.make n (-1)
and default = Array.make n 0
and base_code = Array.make n 0
and backtrk_code = Array.make n 0
and default_code = Array.make n 0 in
for i = 0 to n - 1 do
match state_v.(i) with
| Perform (n,c) ->
......
......@@ -84,7 +84,7 @@ let complement s = diff all_chars s
let env_to_array env = match env with
| [] -> assert false
| (_,x)::rem ->
let res = Array.create 257 x in
let res = Array.make 257 x in
List.iter
(fun (c,y) ->
List.iter
......
......@@ -590,7 +590,7 @@ let rec firstpos = function
(* Berry-sethi followpos *)
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
| Empty|Action _|Tag _ -> ()
| Chars (n,_) -> v.(n) <- s
......@@ -1131,7 +1131,7 @@ let make_tag_entry id start act a r = match a with
| _ -> r
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
(fun (act,m,_) ->
envs.(act) <-
......@@ -1185,7 +1185,7 @@ let make_dfa lexdef =
done ;
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;
(* Useless state reset, so as to restrict GC roots *)
reset_state () ;
......
......@@ -80,7 +80,7 @@ let output_entry sourcefile ic oc oci e =
output_args e.auto_args
(fun oc x ->
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
(output_memory_actions " ") init_moves
e.auto_name
......
......@@ -22,7 +22,7 @@ open Common
let output_auto_defs oc =
fprintf oc "let __ocaml_lex_init_lexbuf lexbuf mem_size =\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_last_pos <- pos ;\n\
lexbuf.Lexing.lex_last_action <- -1\n\
......
......@@ -15,12 +15,12 @@ type 'a t = {mutable next : int ; mutable data : 'a array}
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
;;
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) ;
table.data <- t
......
......@@ -91,12 +91,12 @@ let _ =
let outputfile : string =
match !outputfile with
| None ->
Filename.concat dirname ((String.capitalize basename) ^ "_ml.v")
Filename.concat dirname ((String.capitalize_ascii basename) ^ "_ml.v")
| Some f ->
f
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 *)
let cmd = Printf.sprintf "mkdir -p %s" debugdir in
begin try ignore (Sys.command cmd)
......
......@@ -131,27 +131,20 @@ let str_cmp (s1:string) (s2:string) =
let str_starts_with p s =
let n = String.length p in
String.length s >= n
&& 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
String.length s >= n
&& String.sub s 0 n = p
let str_capitalize_1 s =
if String.length s <= 0 then s else
let s' = String.copy s in
s'.[0] <- Char.uppercase s.[0];
s'
let s' = Bytes.of_string s in
Bytes.set s' 0 (Char.uppercase s.[0]);
Bytes.unsafe_to_string s'
let str_capitalize_2 s =
if String.length s < 2 then s else
let s' = String.copy s in
s'.[1] <- Char.uppercase s.[1];
s'
let s' = Bytes.of_string s in
Bytes.set s' 1 (Char.uppercase s.[1]);
Bytes.unsafe_to_string s'
(**************************************************************)
......
......@@ -53,7 +53,6 @@ val list_index : 'a -> 'a list -> int
val str_cmp : string -> string -> int
val str_starts_with : string -> string -> bool
val str_replace : char -> char -> string -> string
(** Capitalize the first letter of a string (if any) *)
......
......@@ -62,8 +62,9 @@ let parse_file inputfile parse_fun ast_magic =
let ic = open_in_bin inputfile in
let is_ast_file =
try
let buffer = String.create (String.length ast_magic) in
really_input ic buffer 0 (String.length ast_magic);
let buffer =
really_input_string ic (String.length ast_magic)
in
if buffer = ast_magic then true
else if String.sub buffer 0 9 = String.sub ast_magic 0 9 then
raise Outdated_version
......@@ -97,7 +98,7 @@ let process_implementation_file ppf sourcefile =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
let inputfile = preprocess sourcefile in
try
......@@ -118,21 +119,21 @@ let process_implementation_file ppf sourcefile =
(*incr Odoc_global.errors ;*)
None, inputfile
(* ADDED *)
| Env.Error err ->
| Env.Error err ->
Env.report_error ppf err;
print_newline();
raise e
| Typecore.Error (loc,err) ->
| Typecore.Error (loc,err) ->
Location.print_error ppf loc;
Typecore.report_error ppf err;
print_newline();
raise e
| Typetexp.Error (loc,err) ->
| Typetexp.Error (loc,err) ->
Location.print_error ppf loc;
Typetexp.report_error ppf err;
print_newline();
raise e
| Typemod.Error (loc,err) ->
| Typemod.Error (loc,err) ->
Location.print_error ppf loc;
Typemod.report_error ppf err;
print_newline();
......@@ -145,7 +146,7 @@ let process_implementation_file ppf sourcefile =
let process_interface_file ppf sourcefile =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
let inputfile = preprocess sourcefile in
let ast = parse_file inputfile Parse.interface ast_intf_magic_number in
......@@ -160,7 +161,7 @@ let process_interface_file ppf sourcefile =
let typecheck_implementation_file ppf sourcefile parsetree =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
(* let inputfile = preprocess sourcefile in*)
let env = initial_env () in
......@@ -179,21 +180,21 @@ let typecheck_implementation_file ppf sourcefile parsetree =
prerr_endline s;
(*incr Odoc_global.errors ;*)
None
| Env.Error err ->
| Env.Error err ->
Env.report_error ppf err;
print_newline();
raise e
| Typetexp.Error (loc,err) ->
| Typetexp.Error (loc,err) ->
Location.print_error ppf loc;
Typetexp.report_error ppf err;
print_newline();
raise e
| Typecore.Error (loc,err) ->
| Typecore.Error (loc,err) ->
Location.print_error ppf loc;
Typecore.report_error ppf err;
Typecore.report_error ppf err;
print_newline();
raise e
| Typemod.Error (loc,err) ->
| Typemod.Error (loc,err) ->
Location.print_error ppf loc;
Typemod.report_error ppf err;
print_newline();
......@@ -205,7 +206,7 @@ let typecheck_implementation_file ppf sourcefile parsetree =
let typecheck_interface_file ppf sourcefile output_prefix =
init_path ();
let prefixname = Filename.chop_extension sourcefile in
let modulename = String.capitalize(Filename.basename prefixname) in
let modulename = String.capitalize_ascii (Filename.basename prefixname) in
Env.set_unit_name modulename;
let inputfile = preprocess sourcefile in
let ast = parse_file inputfile Parse.interface ast_intf_magic_number in
......@@ -224,21 +225,21 @@ let typecheck_interface_file ppf sourcefile output_prefix =
prerr_endline s;
(*incr Odoc_global.errors ;*)
None
| Env.Error err ->
| Env.Error err ->
Env.report_error ppf err;
print_newline();
raise e
| Typetexp.Error (loc,err) ->
| Typetexp.Error (loc,err) ->
Location.print_error ppf loc;
Typetexp.report_error ppf err;
print_newline();
raise e
| Typecore.Error (loc,err) ->
| Typecore.Error (loc,err) ->
Location.print_error ppf loc;
Typecore.report_error ppf err;
Typecore.report_error ppf err;
print_newline();
raise e
| Typemod.Error (loc,err) ->
| Typemod.Error (loc,err) ->
Location.print_error ppf loc;
Typemod.report_error ppf err;
print_newline();
......
......@@ -96,7 +96,7 @@ let keyword_table =
(* To buffer string literals *)
let initial_string_buffer = String.create 256
let initial_string_buffer = Bytes.create 256
let string_buff = ref initial_string_buffer
let string_index = ref 0
......@@ -105,16 +105,16 @@ let reset_string_buffer () =
string_index := 0
let store_string_char c =
if !string_index >= String.length (!string_buff) then begin
let new_buff = String.create (String.length (!string_buff) * 2) in
String.blit (!string_buff) 0 new_buff 0 (String.length (!string_buff));
if !string_index >= Bytes.length (!string_buff) then begin
let new_buff = Bytes.create (Bytes.length (!string_buff) * 2) in
Bytes.blit (!string_buff) 0 new_buff 0 (Bytes.length (!string_buff));
string_buff := new_buff
end;
String.unsafe_set (!string_buff) (!string_index) c;
Bytes.unsafe_set (!string_buff) (!string_index) c;
incr string_index
let get_stored_string () =
let s = String.sub (!string_buff) 0 (!string_index) in
let s = Bytes.sub_string (!string_buff) 0 (!string_index) in
string_buff := initial_string_buffer;
s
......@@ -171,13 +171,14 @@ let cvt_nativeint_literal s =
let remove_underscores s =
let l = String.length s in
let b = Bytes.create l in
let rec remove src dst =
if src >= l then
if dst >= l then s else String.sub s 0 dst
if dst >= l then s else Bytes.sub_string b 0 dst
else
match s.[src] with
'_' -> remove (src + 1) dst
| c -> s.[dst] <- c; remove (src + 1) (dst + 1)
| c -> Bytes.set b dst c; remove (src + 1) (dst + 1)
in remove 0 0
(* Update the current location with file name and line number. *)
......
......@@ -70,6 +70,8 @@ let status = ref Terminfo.Uninitialised
let num_loc_lines = ref 0 (* number of lines already printed after input *)
(* ARTHUR commented out
(* Highlight the locations using standout mode. *)
let highlight_terminfo ppf num_lines lb loc1 loc2 =
......@@ -81,7 +83,7 @@ let highlight_terminfo ppf num_lines lb loc1 loc2 =
(* Count number of lines in phrase *)
let lines = ref !num_loc_lines in
for i = pos0 to lb.lex_buffer_len - 1 do
if lb.lex_buffer.[i] = '\n' then incr lines