Commit d2268f88 authored by charguer's avatar charguer

fixbug_constructor

parent 3635cd57
lib/stdlib should have make quick target
----------
-- while loop invariant : when b is false, should not prove decrease
Lemma xwhile_inv_basic_lemma :
forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop),
......
# If defined, $(ML) is the list of OCaml source files to consider.
ML := Demo.ml
# Uncomment the next line if you wish to compile only Test.ml.
# ML := Test.ml
# CFML_FLAGS := -debug
include ../Makefile.example
type 'a compare_poly_type =
| CompCst
| CompPoly of 'a
| CompTuple of 'a * bool
| CompFunc of ('a -> 'a)
let compare_poly_custom (x : 'a compare_poly_type) (y : int compare_poly_type) =
let _r1 = (x = CompCst) in
let _r2 = (y = CompPoly 3) in
let _r3 = (y = CompPoly 3) in
let _r4 = (y = CompTuple (3, true)) in
()
let f x = x
\ No newline at end of file
Require Export CFLib Aux_ml.
Require Import Extra.
Lemma f_spec :
Spec f (x:int) |R>> R \[] (fun y => \[same x y]).
Proof.
xcf. intros. xret. unfold same. hsimpl~.
Qed.
Hint Extern 1 (RegisterSpec f) => Provide f_spec.
Require Import LibCore LibInt.
Definition same (x y : int) := (x = y).
open NullPointers
let g x = Auxi.f x
Require Export CFLib Main_ml.
Require Import Auxi_ml Auxi_proof Extra.
Lemma g_spec :
Spec g (x:int) |R>> R \[] (fun y => \[same x y]).
Proof.
xcf. intros. xapp. hsimpl~.
Qed.
Hint Extern 1 (RegisterSpec g) => Provide g_spec.
include ../Makefile.example
# 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
# To save time:
# V := $(filter-out $(PWD)/Demo_proof.v $(PWD)/Demo_ml.v $(PWD)/Test_proof.v $(PWD)/Test_ml.v, $(wildcard $(PWD)/*.v))
V := $(addprefix $(PWD)/, TestDepend_OnlyCoq.v TestDepend_MainCode_proof.v TestDepend_AuxCode_proof.v)
include ../Makefile.example
type t = C | D
let f x = x
Set Implicit Arguments.
Require Export CFLib.
Require Import
TestDepend_OnlyCoq
TestDepend_AuxCode_ml.
Lemma f_spec : forall (A:Type) (x:A),
app f [x] \[] (fun y => \[same x y]).
Proof.
xcf. intros. xret. unfold same. hsimpl~.
Qed.
Hint Extern 1 (RegisterSpec f) => Provide f_spec.
\ No newline at end of file
let g () =
TestDepend_AuxCode.f TestDepend_AuxCode.C
Set Implicit Arguments.
Require Export CFLib.
Require Import
TestDepend_OnlyCoq
TestDepend_AuxCode_ml
TestDepend_AuxCode_proof
TestDepend_MainCode_ml.
Lemma g_spec :
app g [tt] \[] \[= TestDepend_AuxCode_ml.C].
Proof.
xcf. intros. xapp. xsimpl. unfolds same. auto.
Qed.
Hint Extern 1 (RegisterSpec g) => Provide g_spec.
\ No newline at end of file
Set Implicit Arguments.
Require Import LibInt.
Definition same (A:Type) (x y : A) := (x = y).
......@@ -38,7 +38,7 @@ ifeq ($(findstring $(MAKECMDGOALS),clean),)
endif
##############################################################################
# Compilation.
# 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
......@@ -46,13 +46,20 @@ endif
PWD := $(shell pwd)
V := \
$(wildcard $(PWD)/*.v) \
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.
V_AUX := \
$(wildcard $(TLC)/*.v) \
$(wildcard $(CFML)/lib/coq/*.v) \
$(wildcard $(CFML)/lib/stdlib/*.v) \
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 \
......@@ -62,7 +69,7 @@ COQINCLUDE := \
##############################################################################
# Files.
# Options for OCaml.
# TEMPORARY
# READLINK = $(shell if hash greadlink 2>/dev/null ; then echo greadlink ; else echo readlink ; fi)
......@@ -100,9 +107,13 @@ all:
# to proceed unless the previous phase was successful.
# 1. Compile the OCaml code.
@ $(OCAMLBUILD) $(ML_MAIN:.ml=.native)
# 2. Build the characteristic formulae.
# 2. Compile the characteristic formula generator.
@ $(MAKE) -C $(CFML)/generator
# 3. Compile the CFML library
@ $(MAKE) -C $(CFML)/lib/stdlib quick
# 4. Build the characteristic formulae.
@ $(MAKE) --no-print-directory -f $(CFML)/lib/make/Makefile.cfml
# 3. Check the Coq proofs.
# 5. Check the Coq proofs.
# While we're at it, regenerate the _CoqProject file. (Optional.)
@ $(MAKE) -f $(TLC)/Makefile.coq _CoqProject proof
......
......@@ -70,8 +70,11 @@ let lift_module_name id =
(* -- old: if name = "OkaStream" then "CFPrim" else *)
(* Function for adding "_ml" to the modules in a path,
including the last constant which is assumed to a module name *)
(* TODO: rename this function *)
including the last constant which is assumed to a module name.
For example, "Foo.Bar" becomes "Foo_ml.Bar_ml".
TODO: rename this function *)
let rec lift_full_path = function
| Pident id -> Pident (Ident.create (lift_module_name id))
......@@ -79,7 +82,8 @@ let rec lift_full_path = function
| Papply(p1, p2) -> assert false
(* Function for adding "_ml" to the modules in a path,
but not changing the last constant in the path *)
but not changing the last constant in the path.
For example, "Foo.x" becomes "Foo_ml.x". *)
let lift_path = function
| Pident id -> Pident id
......@@ -87,9 +91,7 @@ let lift_path = function
| Papply(p1, p2) -> assert false
(** Translates a path into a string. A module called "Test"
becomes "Test_ml" if it refers to a file, and it becomes
"MLTest" if it refers to a functor argument.
--todo: call them all "Test_ml"? *)
becomes "Test_ml". *)
let lift_full_path_name p =
Path.name (lift_full_path p)
......@@ -238,12 +240,13 @@ let coq_of_constructor loc p c ty =
| _ -> failwith "coq_of_constructor: constructor has a type that is not a type constructor"
in
let x = string_of_path p in
(* TODO: fixme, this can be hacked by rebinding None, Some, or :: ..*)
let coq_name, arity =
match find_builtin_constructor x with
| None -> x, (typ_arity_constr c)
| None -> lift_path_name p, (typ_arity_constr c)
| Some (coq_name,arity) -> coq_name, arity
in
if typs = []
if typs = []
then coq_var coq_name
else coq_apps (coq_var_at coq_name) typs
(* DEPRECATED: coq_app_var_wilds coq_name arity *)
......
......@@ -74,7 +74,8 @@ let _ =
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 && sourcefile <> "Pervasives.ml" then
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 "&&";
......
......@@ -16,11 +16,12 @@ endif
# "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)
export
COQINCLUDE := \
-R $(TLC) TLC \
-R $(CFML)/lib/coq CFML \
-R $(shell pwd) STDLIB
-R $(PWD) STDLIB
##############################################################################
# Files.
......@@ -42,12 +43,16 @@ V_AUX := $(wildcard $(TLC)/*.v) \
.PHONY: all
all: $(CMJ)
all: $(CMJ) $(CFML_MLV)
# Must run in two successive phases, as coqdep must not run until the
# files %_ml.v have been generated. So, we create the files %.cmj and
# %_ml.v first (above), then compile every .v file.
@ $(MAKE) -f $(TLC)/Makefile.coq $@
quick: $(CMJ) $(CFML_MLV)
@ $(MAKE) -f $(TLC)/Makefile.coq $@
##############################################################################
# Generating %.cmj and %_ml.v.
......@@ -63,10 +68,10 @@ CFML_FLAGS :=
# inter-module dependencies. Every module is allowed to implicitly depend
# on Pervasives.
Pervasives_ml.v Pervasives.cmj: Pervasives.ml
$(PWD)/Pervasives_ml.v $(PWD)/Pervasives.cmj: $(PWD)/Pervasives.ml
$(CFML_MLV) $(CFML_FLAGS) -nostdlib -nopervasives -I . $< || (rm -f $@; exit 1)
%_ml.v %.cmj: %.ml Pervasives.cmj
$(PWD)/%_ml.v $(PWD)/%.cmj: $(PWD)/%.ml $(PWD)/Pervasives.cmj
$(CFML_MLV) $(CFML_FLAGS) -nostdlib -I . $< || (rm -f $@; exit 1)
##############################################################################
......
......@@ -7,7 +7,6 @@ Ltac auto_star ::= jauto.
(********************************************************************)
(* ** Heaps *)
(*------------------------------------------------------------------*)
(* ** Representation of heaps *)
......@@ -122,15 +121,6 @@ Notation "'Hexists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
Notation "\GC" := (hprop_gc) : heap_scope.
(* BONUS
Notation "\[= v ]" := (fun x => \[x = v])
(at level 0) : heap_scope.
Notation "P ==+> Q" := (pred_le P%h (hprop_star P Q))
(at level 55, only parsing) : heap_scope.
*)
(********************************************************************)
(* ** Lemmas on states and heaps *)
......@@ -215,11 +205,6 @@ Tactic Notation "rew_disjoint" :=
Tactic Notation "rew_disjoint" "*" :=
rew_disjoint; auto_star.
(*
Hint Extern 1 (\# _ _) => rew_disjoint.
Hint Extern 1 (\# _ _ _) => rew_disjoint.
*)
(********************************************************************)
(* ** Predicate on Heaps *)
......@@ -325,17 +310,6 @@ End HeapProp.
Hint Resolve hprop_empty_prove hprop_empty_st_prove.
(* BONUS
Lemma hprop_star_comm_assoc : comm_assoc hprop_star.
Proof using. apply comm_assoc_prove. apply star_comm. apply star_assoc. Qed.
Lemma hprop_star_post_neutral : forall B (Q:B->hprop),
Q \*+ \[] = Q.
Proof using. extens. intros. rewrite~ hprop_star_empty_r. Qed.
*)
(********************************************************************)
(* ** Rules *)
......@@ -407,7 +381,7 @@ Proof using.
{ auto. }
Qed.
Lemma rule_if_true : forall v t1 t2 H Q,
Lemma rule_if : forall v t1 t2 H Q,
triple (If v = val_int 0 then t2 else t1) H Q ->
triple (trm_if v t1 t2) H Q.
Proof using.
......@@ -419,7 +393,7 @@ Proof using.
{ auto. }
Qed.
Lemma let_rule : forall x t1 t2 H Q Q1,
Lemma rule_let : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
......@@ -536,6 +510,28 @@ Qed.
(* BONUS
Lemma hprop_star_comm_assoc : comm_assoc hprop_star.
Proof using. apply comm_assoc_prove. apply star_comm. apply star_assoc. Qed.
Lemma hprop_star_post_neutral : forall B (Q:B->hprop),
Q \*+ \[] = Q.
Proof using. extens. intros. rewrite~ hprop_star_empty_r. Qed.
*)
(* BONUS
Notation "\[= v ]" := (fun x => \[x = v])
(at level 0) : heap_scope.
Notation "P ==+> Q" := (pred_le P%h (hprop_star P Q))
(at level 55, only parsing) : heap_scope.
*)
(*------------------------------------------------------------------*)
(* ** Normalization of [star] *)
......
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