...
 
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
......
......@@ -28,7 +28,7 @@ struct
(H.hash k) mod (Array.length h)
let create n =
Array.create n []
Array.make n []
let rem h k =
let b = bucket h k in
......
(** Representation of fixed-size circular buffers. *)
module Make (Capa : CapacitySig.S) (Item : InhabType.S) =
......
(*************************************************************************)
(** Graph representation by adjacency lists *)
......@@ -15,7 +10,7 @@ type t = (int list) array
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,9 +23,9 @@ type color = White | Gray | Black
let rec dfs_from g c i =
c.(i) <- Gray;
Graph.iter_edges (fun j ->
Graph.iter_edges g i (fun j ->
if c.(j) = White
then dfs_from g c j) g i;
then dfs_from g c j);
c.(i) <- Black
let dfs_main g rs =
......@@ -40,3 +35,48 @@ let dfs_main g rs =
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.
......@@ -809,143 +809,3 @@ let reachable_imperative g a b =
(********************************************************************)
(** * Reachability by imperative DFS, two-colored *)
(* Note: [E] describes set of edges left to process in the loop *)
Record inv (G:graph unit) n a (C:array bool) L (E:set int) := {
inv_length_C : length C = n;
inv_source : C[a] = true;
inv_stack : forall i, Mem i L -> i \in nodes G /\ C[i] = true;
inv_true_reachable : forall i, i \in nodes G ->
C[i] = true -> reachable G a i;
inv_true_edges : forall i j,
C[i] = true -> has_edge G i j tt ->
Mem i L \/ C[j] = true \/ j \in E }.
Lemma inv_init : forall G n a C,
C = LibArray.make n false -> a \in nodes G ->
inv G n a (C[a:=true]) (a :: nil) \{}.
Proof.
introv EC Ga. constructors.
skip.
skip.
introv H. inverts H as H. skip. inverts H.
introv Gi H. skip_rewrite (i = a).
exists (nil:path unit). constructors*.
introv Ci E. skip_rewrite (i = a). left*.
Qed.
Lemma inv_step_push : forall G n a C L i j js,
inv G n a C L ('{j} \u js) ->
C[i] = true -> has_edge G i j tt ->
inv G n a (C[i:=true]) (i :: L) js.
Proof.
introv I Ci M. inverts I. constructors; auto.
skip.
intros i' M'. skip.
skip. (* extend path with edge at end *)
intros i' j' Ci' E.
(* two cases: i is i' or not. If so, wrote true *)
skip.
Qed.
Lemma inv_step_skip : forall G n a C L j js,
inv G n a C L ('{j} \u js) -> C[j] = true ->
inv G n a C L js.
Proof.
introv I Cj. inverts I. constructors; auto.
intros i' j' Ci' E.
lets [M|[M|M]]: inv_true_edges0 Ci' E; [ eauto | eauto | ].
set_in M; eauto.
Qed.
Lemma inv_end : forall G n a C,
inv G n a C nil \{} ->
forall j, j \in nodes G ->
(reachable G a j <-> C[j] = true).
Proof.
introv I Gj. iff H.
destruct H as [p P]. lets PC: inv_source I. gen P PC.
generalize a as i. intros i P. induction P.
auto.
introv Cx. destruct w. lets [M|[M|M]]: inv_true_edges I Cx H.
inverts M.
auto.
inverts M.
applys* inv_true_reachable.
Qed.
Parameter ml_stack_is_empty_spec : forall a,
Spec ml_stack_is_empty (l:loc) |R>>
forall (L:list a),
keep R (l ~> Stack L) (fun b => \[b = isTrue (L = nil)]).
Hint Extern 1 (RegisterSpec ml_stack_is_empty) => Provide ml_stack_is_empty_spec.
Ltac fix_boolof := fix_bool_of_known tt.
Lemma reachable_imperative_spec :
Spec reachable_imperative g a b |R>>
forall G, a \in nodes G -> b \in nodes G ->
keep R (g ~> GraphAdjList G) (fun r => \[r = isTrue (reachable G a b)]).
Proof.
xcf. instantiate (1:=unit). introv Ga Gb.
xapp. intros Gn. xapp. intros C0 HC0.
xapp. xapp*. xseq. xapp.
set (hinv := fun E CL =>
let '(C,L) := CL in
g ~> GraphAdjList G
\* c ~> Array C
\* s ~> Stack L
\* \[inv G n a C L E]).
set (W := lexico2 (binary_map (count (= true)) (upto n))
(binary_map (fun L:list int => LibList.length L) (downto 0))).
set (K := (fun CL => bool_of (let '(C,L) := CL : array bool * list int in
L <> nil))).
xseq (# Hexists C, hinv \{} (C,nil)).
xwhile_inv W (hinv \{}) K.
skip. (* well_founded W *)
unfold hinv.
evar (X:array bool); evar (Y:list int); exists (X,Y); subst X Y.
hsimpl. apply* inv_init.
intros [C L]. splits.
unfold hinv. xextract as I. xlet. xapps. simpl.
(* todo: cleanup*) xextract. intro_subst. xret.
hsimpl*. unfold K. fix_boolof. rew_reflect*.
xextract as HK I. unfolds in HK. fix_boolof.
xapp*. intros L' HL'. subst L. clear HK.
xfun f. forwards~ [Gi Ci]: inv_stack I i.
xapp_spec* iter_edges_target_of_spec' (fun E => Hexists CL, hinv E CL).
introv E N. xapp_body. clear Sf. intros ?. intro_subst.
clears W K C. clears L'. unfold hinv at 1. xextract. intros [C L]. xextract as I.
xapps. skip. xif.
xapp*. skip. xapp. unfold hinv. hsimpl (C[i:=true],i::L).
applys inv_step_push. eauto. skip. (* come from pop of L' *) eauto.
xret. unfold hinv. hsimpl (C,L). apply* inv_step_skip.
skip. (* ??
unfold hinv. hsimpl (C,L'). hsimpl. *)
hextract as CL HCL. hsimpl CL.
skip. (* termination. *)
unfold K. xextracts. hsimpl*.
clear hinv K W. intros C I. lets: inv_length_C I.
xapp*. hsimpl.
forwards R: inv_end I Gb. subst r. extens. rew_reflect*.
Admitted. (* faster *)
End ReachableImp.
(* Another similar one talking about remaining edges *)
Lemma iter_edges_target_of_spec' :
Spec iter_edges_target_of g i f |R>>
forall (G:graph unit) (I:set int->hprop), i \in nodes G ->
(forall j js, has_edge G i j tt -> j \notin js ->
(App f j;) (I (\{j} \u js)) (# I js)) ->
R (g ~> GraphAdjList G \* I (out_edges_target G i))
(# g ~> GraphAdjList G \* I \{}).
Admitted.
This diff is collapsed.
......@@ -8,6 +8,28 @@ 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 *)
......@@ -795,6 +817,19 @@ type ('a,'b) recordb =
-- 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 *)
......
......@@ -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.
......@@ -427,6 +427,7 @@ let exp_find_inlined_primitive e oargs =
(* _debug(); *)
begin match args with
| [n; {exp_desc = Texp_constant (Const_int m)}]
when m <> 0
&& List.mem name ["Pervasives.mod"; "Pervasives./"] ->
......@@ -700,27 +701,8 @@ let rec cfg_exp env e =
| Texp_construct(p, cstr, args) -> ret e
(* TODO: only in purely function setting: | Texp_record (lbl_expr_list, opt_init_expr) -> ret e*)
| Texp_record (lbl_expr_list, opt_init_expr) ->
if opt_init_expr <> None then unsupported loc "record-with";
let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
let build_arg (name, arg) =
let value = coq_apps coq_dyn_at [coq_typ loc arg; lift arg] in
Coq_tuple [Coq_var (record_field_name name); value]
in
let arg = coq_list (List.map build_arg named_args) in
Cf_record_new (arg)
(* DEPRECATED
let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
let func = Coq_var (pathfront ^ (record_make_name pathend)) in
let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
let args =
try List.map (fun name -> List.assoc name named_args) fields_names
with Not_found -> failwith "some fields are missing in a record construction"
in
let tprod = coq_prod (List.map coq_typ args) in
Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
*)
| Texp_record (_, _) ->
cfg_record env e
| Texp_apply (funct, oargs) when (exp_find_inlined_primitive funct oargs <> None) -> ret e
......@@ -734,6 +716,12 @@ let rec cfg_exp env e =
| Texp_constraint ({exp_desc = Texp_function (_,_,_)},_,_) -> true (* todo: generalize *)
| _ -> false in
let is_let_record_new =
match (snd (List.hd pat_expr_list)).exp_desc with
| Texp_record (_,_) -> true
| Texp_constraint ({exp_desc = Texp_record (_,_)},_,_) -> true (* todo: generalize *)
| _ -> false in
(* binding of functions, possibly mutually-recursive *)
if is_let_fun then begin
let env' = match rf with
......@@ -789,7 +777,13 @@ let rec cfg_exp env e =
begin
let cf1 = cfg_exp env bod in
let cf1 =
(* Recursive record term let-binding *)
if is_let_record_new && rf = Recursive then
cfg_record ~record_name:x env bod
else
cfg_exp env bod
in
let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
(* fvs_typ contains all free type variables in the type;
and thus too many w.r.t. to the ones of interest here *)
......@@ -950,6 +944,33 @@ and cfg_func env fvs pat bod =
(* --todo: check if the set of type variables quantified is not too
conservative. Indeed, some type variables may no longer occur. *)
and cfg_record ?(record_name = "_") env e =
let loc = e.exp_loc in
match e.exp_desc with
| Texp_record (lbl_expr_list, opt_init_expr) ->
if opt_init_expr <> None then unsupported loc "record-with";
let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
let build_arg (name, arg) =
let value = coq_apps coq_dyn_at [coq_typ loc arg; lift_val env arg] in
Coq_tuple [Coq_var (record_field_name name); value]
in
let arg =
Coq_fun ((record_name, coq_var "CFHeaps.loc"),
coq_list (List.map build_arg named_args)) in
Cf_record_new (arg)
(* DEPRECATED
let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
let func = Coq_var (pathfront ^ (record_make_name pathend)) in
let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
let args =
try List.map (fun name -> List.assoc name named_args) fields_names
with Not_found -> failwith "some fields are missing in a record construction"
in
let tprod = coq_prod (List.map coq_typ args) in
Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
*)
| _ -> assert false
(*#########################################################################*)
(* ** Characteristic formulae for modules *)
......@@ -965,8 +986,28 @@ let is_type_abbrev (name,dec) =
let is_type_record (name,dec) =
match dec.typ_type.type_kind with Type_record _ -> true | _ -> false
let rec is_ignored_str_value (pat,exp) =
is_ignored_exp exp
and is_ignored_exp exp =
match exp.exp_desc with
| Texp_constraint (e, _, _) ->
is_ignored_exp e
| Texp_sequence(expr1, expr2) ->
is_ignored_exp expr1
| Texp_function (_, pat_expr_list, _) ->
List.exists is_ignored_str_value pat_expr_list
| Texp_apply ({exp_desc = Texp_ident (f,_d)},
[_, Some {exp_desc = Texp_constant (Const_string "CFML")}, _])
when get_qualified_pervasives_name f = "Pervasives.ignore"
-> true
| _ -> false
(** Generate the top-level Coq declarations associated with
a top-level declaration from a module. *)
a top-level declaration from a module.
If a toplevel definition begins with [ignore "CFML"] in its body,
then the toplevel definition is ignored by CFML altogether. *)
let rec cfg_structure_item s : cftops =
let loc = s.str_loc in
......@@ -974,6 +1015,8 @@ let rec cfg_structure_item s : cftops =
| Tstr_value(rf, fvs, pat_expr_list) ->
reset_local_labels();
if List.exists is_ignored_str_value pat_expr_list then [] (* ignore *) else begin
(* --todo: improve code sharing between local bindings and top-level bindings *)
let is_let_fun (pat,exp) =
match exp.exp_desc with
......@@ -1066,6 +1109,7 @@ let rec cfg_structure_item s : cftops =
end else
unsupported loc ("mutually-recursive values that are not all functions");
end (* for ignored toplevel item *)
| Tstr_type(decls) -> [ Cftop_coqs (cfg_type_decls loc decls) ]
......@@ -1084,9 +1128,9 @@ let rec cfg_structure_item s : cftops =
[ Cftop_val (id, typ) ]
| Tstr_exception(id, decl) ->
[] (* unsupported "exceptions" *)
[] (* unsupported "exceptions" ; could be raise CFML_ignore *)
| Tstr_exn_rebind(id, path) ->
[] (* unsupported "exceptions" *)
[] (* unsupported "exceptions" ; could be raise CFML_ignore *)
| Tstr_recmodule bindings -> unsupported loc "recursive modules"
| Tstr_class _ -> unsupported loc "objects"
......@@ -1642,7 +1686,7 @@ let cfg_file str =
[ Cftop_coqs ([
Coqtop_set_implicit_args;
Coqtop_require [ "Coq.ZArith.BinInt"; "TLC.LibLogic"; "TLC.LibRelation"; "TLC.LibInt"; "TLC.LibListZ"; "CFML.Shared"; "CFML.CFHeaps"; "CFML.CFApp"; "CFML.CFPrint"; "CFML.CFBuiltin" ];
Coqtop_require_import [ "CFML.CFHeader" ];
Coqtop_require_import [ "Coq.ZArith.BinIntDef"; "CFML.CFHeader" ];
Coqtop_custom "Delimit Scope Z_scope with Z.";
Coqtop_custom "Local Open Scope cfheader_scope.";
(*DEPRECATED Coqtop_custom "Open Scope list_scope.";*)
......
......@@ -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)
......
......@@ -134,24 +134,17 @@ let str_starts_with p s =
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
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
......@@ -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
......@@ -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
......
......@@ -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
if Bytes.get lb.lex_buffer i = '\n' then incr lines
done;
(* If too many lines, give up *)
if !lines >= num_lines - 2 then raise Exit;
......@@ -96,7 +98,7 @@ let highlight_terminfo ppf num_lines lb loc1 loc2 =
Terminfo.standout true;
if pos = loc1.loc_end.pos_cnum || pos = loc2.loc_end.pos_cnum then
Terminfo.standout false;
let c = lb.lex_buffer.[pos + pos0] in
let c = Bytes.get lb.lex_buffer (pos + pos0) in
print_char c;
bol := (c = '\n')
done;
......@@ -117,7 +119,7 @@ let highlight_dumb ppf lb loc =
(* Determine line numbers for the start and end points *)
let line_start = ref 0 and line_end = ref 0 in
for pos = 0 to end_pos do
if lb.lex_buffer.[pos + pos0] = '\n' then begin
if Bytes.get lb.lex_buffer (pos + pos0) = '\n' then begin
if loc.loc_start.pos_cnum > pos then incr line_start;
if loc.loc_end.pos_cnum > pos then incr line_end;
end
......@@ -130,7 +132,7 @@ let highlight_dumb ppf lb loc =
let line = ref 0 in
let pos_at_bol = ref 0 in
for pos = 0 to end_pos do
let c = lb.lex_buffer.[pos + pos0] in
let c = Bytes.get lb.lex_buffer (pos + pos0) in
if c <> '\n' then begin
if !line = !line_start && !line = !line_end then
(* loc is on one line: print whole line *)
......@@ -192,6 +194,8 @@ let rec highlight_locations ppf loc1 loc2 =
with Exit -> false
end
*)
(* Print the location in some way or another *)
open Format
......@@ -222,7 +226,7 @@ let print ppf loc =
if startchar < 0 then (0, 1) else (startchar, endchar)
in
if file = "" then begin
if highlight_locations ppf loc none then () else
if false (* ARTHUR highlight_locations ppf loc none *) then () else
fprintf ppf "Characters %i-%i:@."
loc.loc_start.pos_cnum loc.loc_end.pos_cnum
end else begin
......
......@@ -54,7 +54,7 @@ val prerr_warning: t -> Warnings.t -> unit
val echo_eof: unit -> unit
val reset: unit -> unit
val highlight_locations: formatter -> t -> t -> bool
(*val highlight_locations: formatter -> t -> t -> bool*)
(* CFML added *)
......
......@@ -27,7 +27,7 @@ exception Escape_error
let report_error ppf = function
| Unclosed(opening_loc, opening, closing_loc, closing) ->
if String.length !Location.input_name = 0
&& Location.highlight_locations ppf opening_loc closing_loc
&& false (* ARTHUR Location.highlight_locations ppf opening_loc closing_loc *)
then fprintf ppf "Syntax error: '%s' expected, \
the highlighted '%s' might be unmatched" closing opening
else begin
......
......@@ -325,11 +325,11 @@ type primitive_arity =
let inlined_primitives_table =
[
"Pervasives.ignore", (Primitive_unary, "(@CFML.CFBuiltin.ignore _)");
"Pervasives.+", (Primitive_binary, "Coq.ZArith.BinInt.Zplus");
"Pervasives.-", (Primitive_binary, "Coq.ZArith.BinInt.Zminus");
"Pervasives.*", (Primitive_binary, "Coq.ZArith.BinInt.Zmult");
"Pervasives.~-", (Primitive_unary, "Coq.ZArith.BinInt.Zopp");
"Pervasives.abs", (Primitive_unary, "Coq.ZArith.BinInt.Zabs");
"Pervasives.+", (Primitive_binary, "Coq.ZArith.BinInt.Z.add");
"Pervasives.-", (Primitive_binary, "Coq.ZArith.BinInt.Z.sub");
"Pervasives.*", (Primitive_binary, "Coq.ZArith.BinInt.Z.mul");
"Pervasives.~-", (Primitive_unary, "Coq.ZArith.BinInt.Z.opp");
"Pervasives.abs", (Primitive_unary, "Coq.ZArith.BinInt.Z.abs");
"Pervasives.not", (Primitive_unary, "TLC.LibBool.neg");
"Pervasives.fst", (Primitive_unary, "(@Coq.Init.Datatypes.fst _ _)");
"Pervasives.snd", (Primitive_unary, "(@Coq.Init.Datatypes.snd _ _)");
......@@ -349,17 +349,17 @@ let inlined_primitives_table =
"Pervasives.<=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__))");
"Pervasives.>", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__))");
"Pervasives.>=", (Primitive_binary_only_numbers, "(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__))");
"Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmax");
"Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Zmin");
"Pervasives.max", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Z.max");
"Pervasives.min", (Primitive_binary_only_numbers, "Coq.ZArith.BinInt.Z.min");
"List.length", (Primitive_unary, "(@TLC.LibListZ.length _)");
"List.rev", (Primitive_unary, "(@TLC.LibList.rev _)");
"List.concat", (Primitive_unary, "(@TLC.LibList.concat _)");
"List.append", (Primitive_binary, "(@TLC.LibList.app _)");
"Pervasives.@", (Primitive_binary, "(@TLC.LibList.app _)");
]
(* DEPRECATED
"Pervasives.@", (2, "LibList.append");
"List.rev", (1, "LibList.rev");
"List.length", (1, "LibList.length");
"List.append", (2, "LibList.append");
......@@ -592,7 +592,3 @@ let record_unfocus_field_name name =
let cf_axiom_name name =
name ^ "__cf"
......@@ -235,8 +235,9 @@ let check_consistency filename crcs =
let read_pers_struct modname filename =
let ic = open_in_bin filename in
try
let buffer = String.create (String.length cmi_magic_number) in
really_input ic buffer 0 (String.length cmi_magic_number);
let buffer =
really_input_string ic (String.length cmi_magic_number)
in
if buffer <> cmi_magic_number then begin
close_in ic;
raise(Error(Not_an_interface filename))
......
......@@ -678,8 +678,8 @@ let should_extend ext env = match ext with
(* complement constructor tags *)
let complete_tags nconsts nconstrs tags =
let seen_const = Array.create nconsts false
and seen_constr = Array.create nconstrs false in
let seen_const = Array.make nconsts false
and seen_constr = Array.make nconstrs false in
List.iter
(function
| Cstr_constant i -> seen_const.(i) <- true
......
......@@ -19,7 +19,9 @@ type status =
| Bad_term
| Good_term of int
;;
(*ARTHUR
external setup : out_channel -> status = "caml_terminfo_setup";;
external backup : int -> unit = "caml_terminfo_backup";;
external standout : bool -> unit = "caml_terminfo_standout";;
external resume : int -> unit = "caml_terminfo_resume";;
*)
\ No newline at end of file
......@@ -19,7 +19,9 @@ type status =
| Bad_term
| Good_term of int (* number of lines of the terminal *)
;;
(* ARTHUR
external setup : out_channel -> status = "caml_terminfo_setup";;
external backup : int -> unit = "caml_terminfo_backup";;
external standout : bool -> unit = "caml_terminfo_standout";;
external resume : int -> unit = "caml_terminfo_resume";;
*)
\ No newline at end of file
......@@ -126,8 +126,8 @@ let letter = function
| _ -> assert false
;;
let active = Array.create (last_warning_number + 1) true;;
let error = Array.create (last_warning_number + 1) false;;
let active = Array.make (last_warning_number + 1) true;;
let error = Array.make (last_warning_number + 1) false;;
let is_active x = active.(number x);;
let is_error x = error.(number x);;
......
......@@ -444,10 +444,14 @@ Hint Resolve affine_record_repr : affine.
(* Axiomatic specification of [new] on a list of fields;
[app_record_new L] is a characteristic formula describing
the allocation of a record. *)
the allocation of a record.
Definition app_record_new (L:record_descr) : ~~loc :=
local (fun H Q => (fun r => H \* r ~> record_repr L) ===> Q).
[L] takes the name of the record as an argument: this is useful for records
defined recursively, where fields can point to the record itself. In the
non-recursive case, [L] will be of the form [fun _ => ...]. *)
Definition app_record_new (L:loc -> record_descr) : ~~loc :=
local (fun H Q => (fun r => H \* r ~> record_repr (L r)) ===> Q).
(* Remark: taking the definition below would be a bit of a hack,
and it turns out that Coq rejects the definition for universe
......
......@@ -15,7 +15,7 @@ Generalizable Variables A.
Definition char := Ascii.ascii.
Definition array (A:Type) := loc.
Definition array (A:Type) := loc. (* TODO: deprecate *)
......@@ -198,9 +198,9 @@ Qed.
(** Pred / Succ *)
Definition pred (n:int) := (Coq.ZArith.BinInt.Zminus n 1).
Definition pred (n:int) := (Coq.ZArith.BinInt.Z.sub n 1).
Definition succ (n:int) := (Coq.ZArith.BinInt.Zplus n 1).
Definition succ (n:int) := (Coq.ZArith.BinInt.Z.add n 1).
(** Ignore *)
......@@ -212,10 +212,10 @@ Definition ignore A (x:A) := tt.
(* Preventing simplifications *)
Global Opaque
Coq.ZArith.BinInt.Zplus