Commit 19e6ae72 authored by charguer's avatar charguer

Makefile fixed, and generator fixed

parent 26ac5f54
......@@ -22,7 +22,7 @@ all: coqlib generator
$(MAKE) CFMLC=$(CFML)/generator/main.native -C lib/stdlib
coqlib:
$(MAKE) -C lib/coq proof
$(MAKE) CFML=$(CFML) -C lib/coq proof
generator:
rm -f generator/cfml_config.ml
......@@ -33,7 +33,7 @@ generator:
$(MAKE) -C generator
examples: all
$(MAKE) -C examples
$(MAKE) CFML=$(CFML) -C examples
##############################################################################
# Documentation.
......@@ -96,6 +96,8 @@ install: all
mkdir -p $(COQ_CONTRIB)/CFML/Stdlib
install $(CFML)/lib/stdlib/*.vo $(COQ_CONTRIB)/CFML/Stdlib
# "Installation completed."
uninstall:
rm -f $(BINDIR)/cfmlc
# rm -f $(BINDIR)/cfml_cmj
......
Module TESTNEWNOTATIONS.
Notation "'XPRE' H 'XPOST' Q 'XCODE' F" :=
(@tag tag_goal _ F H Q) (at level 69,
format "'[v' '[' 'XPRE' H ']' '/' '[' 'XPOST' Q ']' '/' '[' 'XCODE' F ']' ']'")
: charac.
Notation "F 'XPRE' H 'XPOST' Q" :=
(tag tag_goal F H Q)
(at level 69, H at level 70, only parsing) : charac.
Notation "F 'XINV' H 'XPOST' Q" :=
(tag tag_goal F H%h (Q \*+ H%h))
(at level 69, only parsing,
format "'[v' F '/' '[' 'XINV' H ']' '/' '[' 'XPOST' Q ']' ']'")
: charac.
Notation "F 'XPRE'' H1 'XINV'' H2 'XPOST' Q" :=
(tag tag_goal F (H1 \* H2)%h (Q \*+ H2%h))
(at level 69, only parsing,
format "'[v' F '/' '[' 'XPRE'' H1 ']' '/' '[' 'XINV'' H2 ']' '/' '[' 'XPOST' Q ']' ']'")
: charac.
(*
Notation "F 'XINV'' H2 'XPRE'' H1 'XPOST' Q" :=
(tag tag_goal F (H1 \* H2)%h (Q \*+ H2%h))
(at level 69, only parsing
(*, format "'[v' F '/' '[' 'XPRE'' H1 ']' '/' '[' 'XINV'' H2 ']' '/' '[' 'XPOST' Q ']' ']'" *) )
: charac.
*)
Lemma notation_pre_inv_post_spec_inv : forall (r s:loc) (n m:int),
(app notation_pre_inv_post [r s])
XINV (s ~~> m)
XPRE (r ~~> n)
XPOST (fun x => \[x = m] \* r ~~> (n+1)).
Proof using. xcf. xapp. xapp. xsimpl*. Qed.
Lemma notation_inv_post_spec_pre : forall (r:loc) (n:int),
app notation_inv_post [r]
XPRE (r ~~> n)
XPOST (fun x => \[x = n] \* r ~~> n).
Proof using. xcf. xapp. Qed.
Lemma notation_inv_post_spec_inv : forall (r:loc) (n:int),
app notation_inv_post [r]
XINV (r ~~> n)
XPOST \[= n].
Proof using. xcf. xapp. Qed.
Lemma notation_pre_inv_post_spec_pre : forall (r s:loc) (n m:int),
app notation_pre_inv_post [r s]
XPRE (r ~~> n \* s ~~> m)
XPOST (fun x => \[x = m] \* r ~~> (n+1) \* s ~~> m).
Proof using. xcf. xapp. xapp. xsimpl*. Qed.
End TESTNEWNOTATIONS.
......@@ -11,7 +11,6 @@ Open Scope tag_scope.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* ** Notation for PRE/INV/POST *)
......
......@@ -274,7 +274,7 @@ let rec coqtops_of_imp_cf cf =
| Cf_while (cf1,cf2) ->
let c1 = coq_of_cf cf1 in
let c2 = coq_of_cf cf2 in
let f_core = coq_apps (coq_var "CFML.CFPrint.while") [c1;c2] in
let f_core = coq_apps (coq_var "CFML.CFPrint.cf_while") [c1;c2] in
let f = Coq_app (Coq_var "CFML.CFHeaps.local", f_core) in
coq_tag "tag_while" f
......
......@@ -284,7 +284,7 @@ Notation "F 'PRE' H 'POST' Q" :=
Notation "F 'INV' H 'POST' Q" :=
(tag tag_goal F H%h (Q \*+ H%h))
(at level 69,
(at level 69, only parsing,
format "'[v' F '/' '[' 'INV' H ']' '/' '[' 'POST' Q ']' ']'")
: charac.
......
##############################################################################
# CFML setup.
include ../../Makefile.common
CFML := $(shell cd ../.. && pwd)
include $(CFML)/Makefile.common
##############################################################################
# Compilation.
......
......@@ -72,7 +72,8 @@ CFML_FLAGS :=
ifndef CFMLC
# This should happen only if "make" is run in lib/stdlib.
CFMLC := cfmlc
# DEPRECATED: CFMLC := cfmlc
CFMLC=$(CFML)/generator/main.native
endif
$(PWD)/Pervasives_ml.v $(PWD)/Pervasives.cmj: $(PWD)/Pervasives.ml
......
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