Commit 21e9c1a2 authored by Armaël Guéneau's avatar Armaël Guéneau

Merge remote-tracking branch 'origin/master' into coq-8.6

parents 4a834644 f373f3b2
......@@ -14,9 +14,7 @@ _CoqProject
*.cache
# CFML
*.cmj
lib/tools/cfml_cmj
lib/tools/cfml_dep
lib/tools/cfml_mlv
generator/cfml_config.ml
README.html
lib/coq/README.html
*_ml.v
......
.PHONY: all coqlib tools demos doc clean install
.PHONY: all coqlib generator examples doc clean install uninstall reinstall
CFML := $(shell pwd)
TOOLS := $(CFML)/lib/tools
include Makefile.common
##############################################################################
# Installation destinations.
DEFAULT_PREFIX := $(shell opam config var prefix)
ifeq ($(DEFAULT_PREFIX),)
DEFAULT_PREFIX := /usr/local
endif
PREFIX ?= $(DEFAULT_PREFIX)
BINDIR ?= $(PREFIX)/bin
LIBDIR ?= $(PREFIX)/lib/cfml
##############################################################################
# Targets.
all: coqlib tools
$(MAKE) -C lib/stdlib
all: coqlib generator
$(MAKE) CFMLC=$(CFML)/generator/main.native -C lib/stdlib
coqlib:
$(MAKE) -C lib/coq proof
tools:
generator:
rm -f generator/cfml_config.ml
sed -e 's|@@PREFIX@@|$(PREFIX)|' \
-e 's|@@BINDIR@@|$(BINDIR)|' \
-e 's|@@LIBDIR@@|$(LIBDIR)|' \
generator/cfml_config.ml.in > generator/cfml_config.ml
$(MAKE) -C generator
ln -sf $(CFML)/generator/main.native $(TOOLS)/cfml_mlv
ln -sf $(CFML)/generator/makecmj.native $(TOOLS)/cfml_cmj
ln -sf $(CFML)/generator/myocamldep.native $(TOOLS)/cfml_dep
demos: all
examples: all
$(MAKE) -C examples
##############################################################################
......@@ -40,7 +53,7 @@ clean:
$(MAKE) -C lib/coq $@
$(MAKE) -C lib/stdlib $@
$(MAKE) -C generator $@
rm -rf $(TOOLS)/cfml_mlv $(TOOLS)/cfml_cmj $(TOOLS)/cfml_dep
rm -f generator/cfml_config.ml
rm -f $(DOC)
##############################################################################
......@@ -50,10 +63,46 @@ clean:
# directory to this directory (cfml). Otherwise, perform a copy.
# TEMPORARY, this is TODO
WHERE := $(shell $(COQBIN)coqc -where)
CONTRIB := $(WHERE)/user-contrib
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.
install: all
# Install the generator binary
install -m755 $(CFML)/generator/_build/main.native $(BINDIR)/cfmlc
# install -m755 $(CFML)/generator/_build/makecmj.native $(BINDIR)/cfml_cmj
# Cleanup LIBDIR
rm -rf $(LIBDIR)
# Install the stdlib .cmj files
mkdir -p $(LIBDIR)/stdlib
install $(CFML)/lib/stdlib/*.cmj $(LIBDIR)/stdlib
# Install the auxiliary makefiles
mkdir -p $(LIBDIR)/make
install $(CFML)/lib/make/Makefile.cfml $(LIBDIR)/make
install -m755 $(CFML)/lib/make/ocamldep.post $(LIBDIR)/make
# Cleanup COQ_CONTRIB/CFML
rm -rf $(COQ_CONTRIB)/CFML
# Install the CFML core coq library
mkdir -p $(COQ_CONTRIB)/CFML
install $(CFML)/lib/coq/*.vo $(COQ_CONTRIB)/CFML
# Install the CFML stdlib coq library
mkdir -p $(COQ_CONTRIB)/CFML/Stdlib
install $(CFML)/lib/stdlib/*.vo $(COQ_CONTRIB)/CFML/Stdlib
uninstall:
rm -f $(BINDIR)/cfmlc
# rm -f $(BINDIR)/cfml_cmj
rm -rf $(LIBDIR)
rm -rf $(DOCDIR)
rm -rf $(COQ_CONTRIB)/CFML
install:
rm -rf $(CONTRIB)/CFML
mkdir -p $(CONTRIB)
ln -s `pwd` $(CONTRIB)/CFML
reinstall: uninstall
@ $(MAKE) install
......@@ -5,19 +5,10 @@
# trailing slash), e.g. COQBIN=/var/tmp/coq/bin/.
# If COQBIN is undefined, then "coqc" is used.
# To request installation via a symbolic link, as opposed to
# installation via a copy, define ARTHUR.
# To request creation of .vio files, as opposed to creation of .vo
# files, define SERIOUS=0.
# This assumes that $(CFML) points to the CFML root directory.
SERIOUS := 1
-include $(CFML)/settings.sh
export SERIOUS
export COQBIN
export COQFLAGS
export INCLUDE_TLC_AS_DEPENDENCIES
......
Set Implicit Arguments.
Require Import CFLib CFLibCredits.
Require Import CFML.CFLib CFML.CFLibCredits.
(* Require Import RandomAccessListSig_ml. *)
Require Import BinaryRandomAccessList_ml.
Require Import LibListZ.
Require LibInt.
Require Import TLC.LibListZ.
Require TLC.LibInt.
Module BinaryRandomAccessListSpec (* <: RandomAccessListSigSpec *).
......@@ -150,7 +150,7 @@ Qed.
Lemma inv_ts_len : forall A ts p (L:list A),
inv p ts L ->
ts <> nil ->
ts <> nil ->
2 ^ (p + (length ts) - 1) <= length L.
Proof.
induction ts as [|d ts].
......@@ -209,8 +209,8 @@ Qed.
(** verification *)
(* todo move *)
(* TODO: lemma to rewrite ÷ with / under assumption that args > 0
(* todo move *)
(* TODO: lemma to rewrite ÷ with / under assumption that args > 0
and tactic rew_div pour optimiser. *)
Lemma pow2_succ_div : forall p, p >= 0 -> 2 ^ (p+1) ÷ 2 = 2 ^ p.
......@@ -302,7 +302,7 @@ Proof. xcf. xapp~. Qed.
Hint Extern 1 (RegisterSpec cons) => Provide cons_spec.
Lemma uncons_tree_spec : forall A (ts: rlist_ A) p L,
inv p ts L ->
inv p ts L ->
ts <> nil ->
app uncons_tree [ts]
PRE \[]
......@@ -360,7 +360,7 @@ Qed.
Hint Extern 1 (RegisterSpec tail) => Provide tail_spec.
Import LibInt.
Import TLC.LibInt.
Lemma lookup_tree_spec :
forall a i (t: tree_ a) p L,
......@@ -383,7 +383,7 @@ Qed.
Hint Extern 1 (RegisterSpec lookup_tree) => Provide lookup_tree_spec.
Lemma update_tree_spec :
Lemma update_tree_spec :
forall a i (x: a) (t: tree_ a) p L,
btree p t L ->
ZInbound i L ->
......@@ -406,7 +406,7 @@ Qed.
Hint Extern 1 (RegisterSpec update_tree) => Provide update_tree_spec.
Ltac xapp_xapply_no_simpl K ::=
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
xapply_core K ltac:(fun _ => idtac) ltac:(fun _ => idtac).
Lemma lookup_spec_ind :
......@@ -422,7 +422,7 @@ Proof.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
......@@ -445,30 +445,30 @@ Proof.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
(*
-- strategy 2.
-- strategy 2.
introv. unfold Rlist. generalize 0 as p. revert i L.
induction ts; introv I Bi; inverts I; xcf.
- xgo. apply~ ZInbound_nil_inv.
- { xmatch. xapps~. unpack. subst.
forwards~: length_correct. forwards~: btree_size_correct.
xapps~. xif.
xapp_no_simpl~. (* xapp~ T. *)
xapp_no_simpl~. (* xapp~ T. *)
- apply~ ZInbound_app_l_inv.
- hsimpl. apply~ ZNth_app_l.
- xgo~. apply~ ZInbound_app_r_inv. apply~ ZNth_app_r. }
-- strategy 3.
-- strategy 3.
assert ( de toute la spec )
-- strategy 4
lemme séparée
-- strategy 4
lemme séparée
*)
Qed.
(* OLD
......
Set Implicit Arguments.
Require Import CFLib.
Require Import CFML.CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Import ZsubNoSimpl.
......@@ -1188,7 +1188,7 @@ Abort.
(********************************************************************)
(* ** Recursive function *)
Require Import LibInt.
Require Import TLC.LibInt.
Lemma rec_partial_half_spec : forall k n,
n = 2 * k -> k >= 0 ->
......@@ -1426,7 +1426,7 @@ Qed.
(********************************************************************)
(* ** Arrays *)
Require Import Array_proof LibListZ.
Require Import Array_proof TLC.LibListZ.
Section Array.
......
# CFML := ../../..
# include $(CFML)/Makefile.common
#
# ML := Demo.ml TestDepend_AuxCode.ml TestDepend_MainCode.ml
# PWD := $(shell pwd)
# V := $(wildcard $(PWD)/*.v)
#
# V_AUX := \
# $(wildcard $(TLC)/*.v) \
# $(wildcard $(CFML)/lib/coq/*.v) \
# $(wildcard $(CFML)/lib/stdlib/*.v) \
#
# CFML_FLAGS := -debug
# ML := TestDepend_AuxCode.ml TestDepend_MainCode.ml
# For tests, use:
# ML := Test.ml
# V := $(PWD)/Test_ml.v $(PWD)/Test_proof.v
# To exclude some files:
# V := $(filter-out $(PWD)/Demo_proof.v $(PWD)/Demo_ml.v $(PWD)/Test_proof.v $(PWD)/Test_ml.v, $(wildcard $(PWD)/*.v))
# To include some files:
# V := $(addprefix $(PWD)/, TestDepend_OnlyCoq.v TestDepend_MainCode_proof.v TestDepend_AuxCode_proof.v)
include ../Makefile.example
EXAMPLE_DIRS = \
Demos \
Tuto \
BinaryRandomAccessList \
BinaryRandomAccessList \
# TO FIX:
# BatchedQueue => OCaml complains about ungeneralized type variable (!?)
......
##############################################################################
#
# This script is meant to be included by immediate subfolders of
# $(CFML)/examples.
# This Makefile is meant to be included by immediate subfolders of
# examples.
#
# We assume that CFML has been installed.
#
# Optionally, the variable $(ML) can be used to specify which sources
# to build characteristic formulae for.
......@@ -17,8 +19,8 @@
# Optionally, $(OCAML_FLAGS) can be set (e.g. to "-rectypes").
#
# Optionally, $(CFML_FLAGS) can be set (e.g. to "-debug").
#
# The file $(CFML)/settings.sh may define $(COQBIN).
CFML := $(shell cfmlc -where)
##############################################################################
......@@ -26,47 +28,22 @@
export
##############################################################################
# CFML setup.
# The variable TLC is used to find $(TLC)/Makefile.coq.
# Path to CFML relative to immediate subfolders of $(CFML)/examples.
CFML := ../..
include $(CFML)/Makefile.common
ifeq ($(findstring $(MAKECMDGOALS),clean),)
include $(CFML)/lib/make/Makefile.tools
endif
TLC := $(shell $(COQBIN)coqc -where)/user-contrib/TLC
##############################################################################
# Options for CFML.
# The line "-R $(TLC) TLC" is required only if we wish to write just
# "LibFoo", as opposed to "TLC.LibFoo". In the long run, I believe it
# would be preferable to explicitly use the TLC prefix.
PWD := $(shell pwd)
ifndef V
V := $(wildcard $(PWD)/*.v)
endif
# By default, V_AUX contains all of TLC and CFML libraries;
# additional files may be provided in the $(V_AUX_EXAMPLE) command.
ifndef V_AUX
V_AUX := \
$(wildcard $(TLC)/*.v) \
$(wildcard $(CFML)/lib/coq/*.v) \
$(wildcard $(CFML)/lib/stdlib/*.v) \
$(V_AUX_EXAMPLE)
endif
COQINCLUDE := \
-R $(TLC) TLC \
-R $(CFML)/lib/coq CFML \
-R $(CFML)/lib/stdlib STDLIB \
-R $(PWD) EXAMPLE
-R $(shell $(COQBIN)coqc -where)/user-contrib/CFML/Stdlib CFML.Stdlib \
-R $(PWD) EXAMPLE \
##############################################################################
# Options for OCaml.
......@@ -77,7 +54,6 @@ endif
ifndef OCAML_INCLUDE
OCAML_INCLUDE := \
-I $(CFML)/lib/stdlib \
-I $(PWD)
endif
......@@ -103,13 +79,9 @@ all:
# to proceed unless the previous phase was successful.
# 1. Compile the OCaml code.
@ $(OCAMLBUILD) $(ML_MAIN:.ml=.native)
# 2. Compile the characteristic formula generator.
@ $(MAKE) -C $(CFML)/generator
# 3. Compile the CFML library.
@ $(MAKE) -C $(CFML)/lib/stdlib
# 4. Build the characteristic formulae.
@ $(MAKE) --no-print-directory -f $(CFML)/lib/make/Makefile.cfml
# 5. Check the Coq proofs.
# 2. Build the characteristic formulae.
@ $(MAKE) --no-print-directory -f $(CFML)/make/Makefile.cfml
# 3. Check the Coq proofs.
# While we're at it, regenerate the _CoqProject file. (Optional.)
@ $(MAKE) -f $(TLC)/Makefile.coq _CoqProject proof
......@@ -118,6 +90,6 @@ all:
clean:
rm -rf _build *.native
@make CFML=$(CFML) -f $(CFML)/lib/make/Makefile.cfml $@
@make -f $(CFML)/make/Makefile.cfml $@
$(MAKE) -f $(TLC)/Makefile.coq $@
rm -f _CoqProject
Set Implicit Arguments.
Require Import CFLib Pervasives_ml Pervasives_proof Array_proof Tuto_ml.
Require Import LibListZ.
Require Import CFML.CFLib.
Require Import Stdlib.
Require Import Array_proof.
Require Import Tuto_ml.
Require Import TLC.LibListZ.
(***********************************************************************)
......@@ -43,7 +46,7 @@ Shortcut:
- [xrets] like [xret; xsimpl]
- [xapps] like [xapp; xextracts]
- [tactic~] like [tactic; eauto with maths]
*)
*)
(***********************************************************************)
......@@ -52,7 +55,7 @@ Shortcut:
(** Factorial *)
Parameter facto : int -> int.
Parameter facto_zero : facto 0 = 1.
Parameter facto_zero : facto 0 = 1.
Parameter facto_one : facto 1 = 1.
Parameter facto_succ : forall n, n >= 1 -> facto n = n * facto(n-1).
......@@ -122,13 +125,13 @@ Lemma example_let_spec : forall n,
PRE \[]
POST (fun (v:int) => \[v = 2*n]). (* POST \[= (2 * n)] *)
Proof using.
dup 2.
{ xcf.
xlet. xret. simpl. xpull. intros Ha.
dup 2.
{ xcf.
xlet. xret. simpl. xpull. intros Ha.
xlet. xret. simpl. xpull. intros Hb.
xret. (*hnf.*) xsimpl. math. }
{ xcf. xret ;=> Ha. xret. intros Hb. xret. xsimpl. math. }
(* use: [xcf], [xret], [xsimpl], [math];
(* use: [xcf], [xret], [xsimpl], [math];
[xlet] is optional; if used then [xpull] is also needed. *)
Qed.
......@@ -140,7 +143,7 @@ let example_incr r =
let example_incr r =
let x0__ := get r in
set r (x0__ + 1)
set r (x0__ + 1)
----*)
......@@ -159,13 +162,13 @@ Qed.
(*
Let x0__ := app get [r] in
app set [r (x0__ + 1)]
app set [r (x0__ + 1)]
*)
(* Remark: here are the specifications of get and set from Pervasives_proof.
Lemma get_spec : forall A (v:A) r,
app get [r]
app get [r]
PRE (r ~~> v)
POST (fun x => \[x = v] \* r ~~> v)
......@@ -193,13 +196,13 @@ Lemma example_two_ref_spec : forall n: int,
Proof using.
(*
dup 3.
{xcf. xlet. xapp. simpl. xpull. intros.
xapp.
{xcf. xlet. xapp. simpl. xpull. intros.
xapp.
xapp.
xapp.
xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
}
{xcf. xgo. subst. math. }
}
{xcf. xgo. subst. math. }
*)
......@@ -207,15 +210,15 @@ Proof using.
xcf. xapp. xapp. xapp. xapp. xapps. xapps. xapps. xapps. xapps. xret. xsimpl. math.
Qed.
(*
(*
app example_two_ref [n]
PRE \[]
POST (fun (v:int) => \[v = n+1]).
(* </EXO> *)
Proof using.
(* <EXO> *)
dup.
dup.
{ xcf.
xapps.
xapps.
......@@ -258,7 +261,7 @@ Proof using.
xfor_inv (fun i => r ~~> (facto (i-1))).
{ math. }
{ xsimpl. forwards: facto_zero. easy. }
{ =>> Hi. xapps. xapps. xsimpl.
{ =>> Hi. xapps. xapps. xsimpl.
rew_maths. rewrite (@facto_succ i). ring. math. }
xapps. xsimpl. rew_maths. auto.
Qed.
......@@ -269,7 +272,7 @@ Qed.
I a initial invariant
I i -> I (i+1) when executing [t] on some [i] in the range from [a] to [b]
I (b+1) final invariant
*)
......@@ -326,19 +329,19 @@ Proof using.
(* <EXO> *)
=>> Hn. xcf. xapps. xapps.
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1)) ).
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1)) ).
{ math. }
{ xsimpl. rewrite fib_base. math. math. rewrite~ fib_base. (*math. math.*) }
{ =>> Hi. xapps. xapps. xrets. xapps. xapps. xapps. xsimpl.
{ =>> Hi. xapps. xapps. xrets. xapps. xapps. xapps. xsimpl.
rew_maths. rewrite~ (@fib_succ (i+2)). rew_maths. math_rewrite ((i + 2)-1 = i+1). math. }
xapps. xsimpl~.
xapps. xsimpl~.
(* </EXO> *)
Qed.
(*----Alternative script:
=>> Hn. xcf. xapps. xapps.
=>> Hn. xcf. xapps. xapps.
xfor_inv (fun i => a ~~> (fib i) \* b ~~> (fib (i+1))).
{ math. }
{ xsimpl.
......@@ -349,7 +352,7 @@ Qed.
xapps. xsimpl. auto.
*)
(***********************************************************************)
(** While loops *)
......@@ -547,8 +550,8 @@ module StackList = struct
let pop s =
match s.items with
| hd::tl ->
s.items <- tl;
| hd::tl ->
s.items <- tl;
s.size <- s.size - 1;
hd
| [] -> assert false
......@@ -562,9 +565,9 @@ Import StackList_ml.
(** Definition of [r ~> Stack L], which is a notation for [Stack L r] of type [hprop] *)
Definition Stack A (L:list A) r :=
Hexists n,
r ~> `{ items' := L; size' := n }
Definition Stack A (L:list A) r :=
Hexists n,
r ~> `{ items' := L; size' := n }
\* \[ n = length L ].
......@@ -599,12 +602,12 @@ Proof using.
Qed.
Lemma size_spec : forall (A:Type) (L:list A) (s:loc),
app size [s]
app size [s]
INV (s ~> Stack L)
POST (fun n => \[n = length L]).
(* Remark: the above is a notation for:
app size [s]
app size [s]
PRE (s ~> Stack L)
POST (fun n => \[n = length L] \* s ~> Stack L).
*)
......@@ -613,7 +616,7 @@ Proof using.
xcf.
xopen s. xpull ;=> n Hn. xapp. => m. xpull ;=> E.
xclose s. auto. xsimpl. math.
Unshelve. solve_type. (* todo: xcf A *)
Unshelve. solve_type. (* todo: xcf A *)
Qed.
Lemma length_zero_iff_nil : forall A (L:list A),
......@@ -644,7 +647,7 @@ Proof using.
(* <EXO> *)
xcf.
xopen s. (* Same as [xchange (@Stack_open s)] *)
xpull ;=> n Hn.
xpull ;=> n Hn.
xapps. xapps. xapps. xapp.
xclose s. (* Same as [xchange (@Stack_close s)] *)
rew_list. math.
......
.PHONY: all clean mli
.PHONY: all clean
ML_DIRS := lex parsing tools typing utils
ML_DIRS := lex parsing typing utils
OCAMLBUILD := ocamlbuild -j 4 -classic-display \
$(addprefix -I ,$(ML_DIRS)) \
-cflags "-g" -lflags "-g" \
-use-ocamlfind -package pprint
all:
$(OCAMLBUILD) main.native makecmj.native myocamldep.native
$(OCAMLBUILD) main.native makecmj.native
clean:
rm -rf _build
rm -f *.native
rm -f *~
# An example of generating an .mli file from an .ml file.
# Use with [make BASE=foobar mli].
mli: all
cd _build && \
ocamlfind ocamlc $(addprefix -I ,$(ML_DIRS)) -package pprint \
-i $(BASE).ml > ../$(BASE).mli
let libdir = "@@LIBDIR@@"
This diff is collapsed.
......@@ -8,7 +8,7 @@ open Mytools
let is_tracing = ref false
let trace s =
if !is_tracing
if !is_tracing
then (print_string s; print_newline())
let ppf = Format.std_formatter
......@@ -26,9 +26,11 @@ let outputfile = ref None
(*#########################################################################*)
let (^/) = Filename.concat
let spec =
Arg.align [
("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
" includes a directory where to look for interface files");
("-rectypes", Arg.Set Clflags.recursive_types, " activates recursive types");
("-left2right", Arg.Set Mytools.use_left_to_right_order, " use the left-to-right evaluation order for sub-expressions, instead of OCaml order");
......@@ -40,6 +42,8 @@ let spec =
("-only_normalize", Arg.Set only_normalize, " only generate the .cmj file, and attempt normalization, not the .v file");
("-debug", Arg.Set is_tracing, " trace the various steps");
("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file");
("-where", Arg.Unit (fun () -> print_endline Cfml_config.libdir; exit 0),
" print CFML's library files location and exit");
]
(*
......@@ -53,7 +57,7 @@ let _ =
(*---------------------------------------------------*)
trace "1) parsing of command line";
let files = ref [] in
Arg.parse
Arg.parse
spec
(fun f -> files := f::!files)
("usage: [-I dir] [..other options..] file.ml");
......@@ -65,20 +69,19 @@ let _ =
*)
Clflags.strict_sequence := true;
(* todo: improve the path to mystdlib *)
let gen_dir = Filename.dirname Sys.argv.(0) in
if not !no_mystd_include
then Clflags.include_dirs := (gen_dir ^ "/../lib/ocaml")::!Clflags.include_dirs;
if not !no_mystd_include then
Clflags.include_dirs :=
(Cfml_config.libdir ^/ "stdlib") :: !Clflags.include_dirs;
trace "1) parsing of command line";
if List.length !files <> 1 then
failwith "Expects one argument: the filename of the ML source file";
let sourcefile = List.hd !files in
if !Clflags.nopervasives
if !Clflags.nopervasives
&& Filename.basename sourcefile <> "Pervasives.ml" then
failwith "Option -nopervasives may only be used to compile file Pervasives";
(* this defensive check is needed for the correctness of normalization
of special operators such as "mod" or "&&";
(* this defensive check is needed for the correctness of normalization
of special operators such as "mod" or "&&";
see also function [add_pervasives_prefix_if_needed] *)
if not (Filename.check_suffix sourcefile ".ml") then
......@@ -98,7 +101,7 @@ let _ =
let cmd = Printf.sprintf "mkdir -p %s" debugdir in
begin try ignore (Sys.command cmd)
with _ -> Printf.printf "Could not create debug directory\n" end;
(*---------------------------------------------------*)
trace "2) reading and typing source file";
......@@ -108,7 +111,7 @@ let _ =
| None -> failwith "Could not read and typecheck input file"
|