Commit a9a338dd authored by charguer's avatar charguer

progress

parent 63fc4222
......@@ -15,17 +15,10 @@ CFML := ./
# ------------------------------------------------------------------------------
PWD := $(shell pwd)
MLI_STDLIB := $(filter-out generator/stdlib/camlinternal% \
%genlex.mli %moreLabels.mli %oo.mli, \
$(wildcard generator/stdlib/*.mli))
MLI_ADDED := lib/ocaml/NullPointers.mli lib/ocaml/StrongPointers.mli
MLI := $(MLI_STDLIB) $(MLI_STDLIB)
MAKECMJ := $(PWD)/generator/makecmj.native
MYOCAMLDEP := $(PWD)/generator/myocamldep.native
ONEOCAMLLIBFILE := lib/ocaml/Array.mli
# ------------------------------------------------------------------------------
all: gen coqlib ocamllib
......@@ -52,23 +45,17 @@ clean_ocamllib:
make MAKECMJ=$(MAKECMJ) MYOCAMLDEP=$(MYOCAMLDEP) -C lib/ocaml clean
#*********arguments above should not be needed
clean_ocamllib_full:
@cd lib/ocaml && rm -f $(notdir $(MLI_STDLIB))
@echo "Deleted ocamllib mli files"
clean_coqlib:
make -C lib/coq clean
clean: clean_gen clean_ocamllib clean_coqlib
clean_full: clean clean_ocamllib_full
# ------------------------------------------------------------------------------
# Copy the OCaml standard library mli files
init_ocamllib:
cp $(MLI_STDLIB) lib/ocaml
make MAKECMJ=$(MAKECMJ) MYOCAMLDEP=$(MYOCAMLDEP) -C lib/ocaml init
# Among other things, install a symlink to TLC, since we know where it is.
......
# Possible to define "ML" to be the list of source files to consider
include ../Makefile.example
ML_MAIN := BinarySearchTree.ml TreeCopy.ml Dom.ml
GENERATOR_FLAGS := -rectypes
V_IGNORED := TreeCopy_proof.v
include ../Makefile.example
......@@ -4,6 +4,7 @@ Require Import CFLib TreeCopy_ml.
(********************************************************************)
(** Representation predicate for trees *)
(*
(** Model of imperative trees: functional trees *)
Inductive tree A :=
......@@ -135,6 +136,6 @@ Admitted.
(*(fun l' => l ~> Tree T E \* l' ~> Tree T E).*)
*)
open Aux (* required for cfml to do the require in Coq, in the current implementation *)
open NullPointers
let g x = Aux.f x
\ No newline at end of file
let g x = Aux.f x
let n = null
\ No newline at end of file
# Possible to define "ML" to be the list of source files to consider
# Possible to define "ML_MAIN" to be the list of source files to compile using ocamlbuild
include ../Makefile.example
\ No newline at end of file
EXAMPLE_DIRS=\
DemoMake
DemoMake \
BinaryTrees
# \
#
# BasicDemos
......
......@@ -25,6 +25,7 @@ CFML := ../../
-include $(CFML)/settings.sh
##############################################################
# Default target files
......@@ -46,24 +47,35 @@ ifndef TLC
endif
#*** TODO: remplacer là où il faut CFML par PREFIX
##############################################################
# All
all: cf proof
all: code cf proof
# code
##############################################################
# Program compilation
OCAMLBUILD := $(OCAMLBIN)ocamlbuild
OCAMLBUILD_WITH_OPTIONS := $(OCAMLBUILD) -classic-display -use-ocamlfind -cflags "-g" -lflags "-g"
OCAMLBUILD_WITH_OPTIONS := $(OCAMLBUILD) -I lib -cflag -rectypes -classic-display -use-ocamlfind -cflags "-g" -lflags "-g"
lib:
ln -s $(PREFIX)/lib/ocaml lib
%.native: $(ML)
$(OCAMLBUILD_WITH_OPTIONS) $(basename $<).native
# %.native: lib
#
#%.native: $(ML)
# $(OCAMLBUILD_WITH_OPTIONS) $(basename $<).native
#
# code: $(ML_MAIN:.ml=.native)
code: $(ML_MAIN).native
code: lib $(ML)
$(OCAMLBUILD_WITH_OPTIONS) $(ML_MAIN:.ml=.native)
##############################################################
......@@ -97,7 +109,17 @@ COQC := $(COQBIN)coqc
COQDEP := $(COQBIN)coqdep
COQIDE := $(COQBIN)coqide
ifndef V
V := $(wildcard *.v)
endif
ifdef V_IGNORED
V := $(filter-out $(V_IGNORED),$(V))
endif
test:
echo $(V)
VO := $(patsubst %.v,%.vo,$(V))
VIO := $(patsubst %.v,%.vio,$(V))
VD := $(patsubst %.v,%.v.d,$(V))
......
......@@ -37,12 +37,18 @@ ifndef PREFIX
PREFIX := $(CFML)
endif
ifndef GENERATOR_FLAGS
GENERATOR_FLAGS :=
# e.g. -rectypes
endif
COQINCLUDE:= -R $(PREFIX)/lib/coq/ CFML -R $(PREFIX)/lib/tlc/ TLC -R . EXAMPLE
# ------------------------------------------------------------------------------
# The CFML generator.
GENERATOR := $(CFML)/bin/cfml
GENERATOR := $(CFML)/bin/cfml $(GENERATOR_FLAGS) -rectypes
# Standard tools.
OCAMLDEP := ocamldep
......
......@@ -41,7 +41,8 @@ let dependencies (line : string) : string list =
let is_stdlib_module (m : string) =
(***** TODO: hack because it didn't work *)
if (m = "Array.cmj" || m = "List.cmj") then true else
if (m = "NullPointers" || m = "StrongPointers") then true else
if (m = "Array" || m = "List") then true else
let m = String.uncapitalize m in
try
let cfml = Sys.getenv "CFML" in
......
......@@ -3,32 +3,70 @@
##*********TODO: errors below should not occur if target is "clean".
##*********TODO: error should appear if *.mli files have not been initialized
CFML := ../..
MLI_STDLIB := $(filter-out %generator/stdlib/camlinternal% \
%genlex.mli %moreLabels.mli %oo.mli, \
$(wildcard $(CFML)/generator/stdlib/*.mli))
MLI_EXTRA := $(wildcard $(CFML)/lib/ocaml_extra/*.mli)
ML_EXTRA := $(wildcard $(CFML)/lib/ocaml_extra/*.ml)
MLI := $(notdir $(MLI_STDLIB) $(MLI_EXTRA))
CMJ := $(patsubst %.mli,%.cmj,$(MLI))
# We assume MAKECMJ is defined externally.
ifndef MAKECMJ
$(error Please define MAKECMJ)
MAKECMJ := $(CFML)/generator/makecmj.native
# $(error Please define MAKECMJ)
endif
# We assume MYOCAMLDEP is defined externally.
ifndef MYOCAMLDEP
$(error Please define MAKECMJ)
MYOCAMLDEP := $(CFML)/generator/myocamldep.native
# $(error Please define MAKECMJ)
endif
MLI := $(wildcard *.mli)
CMJ := $(patsubst %.mli,%.cmj,$(MLI))
.PHONY: all
.PHONY: all init
all: $(CMJ)
#*** todo: alternative to initialize
init:
@cp $(MLI_STDLIB) $(MLI_EXTRA) .
@cp $(ML_EXTRA) .
@echo "Copied mli files to lib/ocaml"
# $(MLI):
#  $(error Need to call 'make init' before)
#*** todo: alternative to copy the files on the fly
#
# %.mli: $(CFML)/generator/stdlib/%.mli
# cp $< $@
#
# %.mli: $(CFML)/lib/ocaml_extra/%.mli
# cp $< $@
pervasives.cmj: pervasives.mli
$(MAKECMJ) -nostdlib -nopervasives $<
%.cmj: %.mli pervasives.cmj
$(MAKECMJ) -nostdlib $<
-include .depend
ifeq ($(findstring $(MAKECMDGOALS),init clean),)
-include .depend
endif
.depend: $(MLI)
@$(MYOCAMLDEP) $^ > $@
clean:
rm *.cmj
\ No newline at end of file
rm -f *.mli *.cmj
\ No newline at end of file
......@@ -29,12 +29,20 @@ else
fi
COQINCLUDE="-R ${TLC} TLC -R ${CFML}/lib/coq CFML"
PWD=`pwd`
if [[ ${FILE} == *"examples/"* ]]
then
EXAMPLE_PATH="$(dirname ${FILE})"
COQINCLUDE="${COQINCLUDE} -R ${EXAMPLE_PATH} EXAMPLE"
fi
if [[ ${PWD} == *"examples/"* ]]
then
EXAMPLE_PATH="${PWD}"
COQINCLUDE="${COQINCLUDE} -R ${EXAMPLE_PATH} EXAMPLE"
fi
echo ${COQBIN}coqide ${COQINCLUDE} ${FILE}
${COQBIN}coqide ${COQINCLUDE} ${FILE}
......
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