Commit 9cd45800 authored by POTTIER Francois's avatar POTTIER Francois
parents d24ceb7b cdf1a6e8
......@@ -4,6 +4,18 @@ CFML := $(shell pwd)
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.
......@@ -14,6 +26,11 @@ coqlib:
$(MAKE) -C lib/coq proof
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
examples: all
......@@ -36,6 +53,7 @@ clean:
$(MAKE) -C lib/coq $@
$(MAKE) -C lib/stdlib $@
$(MAKE) -C generator $@
rm -f generator/cfml_config.ml
rm -f $(DOC)
##############################################################################
......
let libdir = "@@LIBDIR@@"
......@@ -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"
| Some (parsetree1, (typedtree1,_)) -> parsetree1
in
file_put_contents (debugdirBase ^ "_original.ml") (Print_past.string_of_structure parsetree1);
file_put_contents (debugdirBase ^ "_original.ml") (Print_past.string_of_structure parsetree1);
if !only_cmj then begin
trace "3) exiting since -only_cmj";
......@@ -118,19 +121,19 @@ let _ =
(*---------------------------------------------------*)
trace "3) normalizing source code";
let parsetree2 : Parsetree.structure = normalize_structure parsetree1 in
file_put_contents (debugdirBase ^ "_normalized.ml") (Print_past.string_of_structure parsetree2);
file_put_contents (debugdirBase ^ "_normalized.ml") (Print_past.string_of_structure parsetree2);
(*---------------------------------------------------*)
trace "4) typing normalized code";
let (typedtree2, _ : Typedtree.structure * Typedtree.module_coercion) =
let fail () =
let (typedtree2, _ : Typedtree.structure * Typedtree.module_coercion) =
let fail () =
failwith (Printf.sprintf "Could not typecheck the normalized source code\nCheck out the file %s_normalized.ml." debugdirBase) in
try
try
match typecheck_implementation_file ppf sourcefile parsetree2 with
| None -> fail() (* TODO: useful?*)
| Some typedtree2 -> typedtree2
with Typetexp.Error(loc, err) -> fail()
in
in
(*---------------------------------------------------*)
trace "5) dumping normalized file";
......@@ -145,9 +148,9 @@ let _ =
(*---------------------------------------------------*)
trace "5) constructing caracteristic formula ast";
let cftops =
try Characteristic.cfg_file typedtree2
with
let cftops =
try Characteristic.cfg_file typedtree2
with
| Typetexp.Error(_, _) -> assert false
| Characteristic.Not_in_normal_form (loc, s) ->
Location.print_error Format.std_formatter loc;
......@@ -162,11 +165,11 @@ let _ =
(*---------------------------------------------------*)
trace "7) dumping debug formula file";
let result = Print_coq.tops coqtops in
file_put_contents (debugdirBase ^ "_formulae.v") result;
file_put_contents (debugdirBase ^ "_formulae.v") result;
(*---------------------------------------------------*)
trace "8) dumping .v file";
file_put_contents outputfile result;
file_put_contents outputfile result;
(*---------------------------------------------------*)
trace "9) characteristic formulae successfully generated\n"
......
......@@ -14,35 +14,35 @@ let no_mystd_include = ref false
(*#########################################################################*)
let (^/) = Filename.concat
let _ =
Settings.configure();
(*---------------------------------------------------*)
let files = ref [] in
Arg.parse
[ ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
Arg.parse
[ ("-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");
("-nostdlib", Arg.Set no_mystd_include, "do not include standard library");
("-nopervasives", Arg.Set Clflags.nopervasives, "do not include standard pervasives file") ]
("-nopervasives", Arg.Set Clflags.nopervasives, "do not include standard pervasives file");
("-where", Arg.Unit (fun () -> print_endline Cfml_config.libdir; exit 0),
"print CFML's library files location and exit");
]
(fun f -> files := f::!files)
("usage: [-I dir] [..other options..] file.mli");
Clflags.strict_sequence := true;
if not !no_mystd_include then
Clflags.include_dirs :=
(Cfml_config.libdir ^/ "stdlib") :: !Clflags.include_dirs;
(* 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 ^ "/camllib")::!Clflags.include_dirs;
if List.length !files <> 1
if List.length !files <> 1
then failwith "Expects one argument: the filename of the MLI file";
let sourcefile = List.hd !files in
let extension = String.sub sourcefile (String.length sourcefile - 3) 3 in
if extension <> "mli"
if not (Filename.check_suffix sourcefile ".mli")
then failwith "Extension should be .mli";
let _basename = String.sub sourcefile 0 (String.length sourcefile - 4) in
let output_prefix = Misc.chop_extension_if_any sourcefile (* _basename ^ ".cmj"*) in
let output_prefix = Misc.chop_extension_if_any sourcefile in
typecheck_interface_file ppf sourcefile output_prefix;
Printf.printf "Wrote %s.cmj\n" output_prefix
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment