Commit 41cf4b36 authored by MARCHE Claude's avatar MARCHE Claude

Prover: updated Makefile

parent 3c3019a6
module Func
use export HighOrd
predicate extensionalEqual (f g:func 'a 'b) =
forall x:'a. f x = g x
(* Assume extensionality of function. *)
axiom functionExtensionality : forall f g:func 'a 'b.
extensionalEqual f g -> f = g
axiom functionExtensionality "W:non_conservative_extension:N" :
forall f g:func 'a 'b. extensionalEqual f g -> f = g
(* Mainly for use in whyml *)
function eval (f:func 'a 'b) (x:'a) : 'b = f x
(* Abstraction definition axiom :
update (f:func 'a 'b) (x:'a) (y:'b) : func 'a 'b =
(\ z:'a. if x = z then y else f z) *)
function update (f:func 'a ~'b) (x:'a) (y:'b) : func 'a 'b
axiom update_def : forall f:func 'a 'b,x:'a,y:'b,z:'a.
update f x y z = if x = z then y else f z
function ([<-])(f:func 'a 'b) (x:'a) (y:'b) : func 'a 'b = update f x y
lemma update_eq : forall f:func 'a 'b,x:'a,y:'b.
update f x y x = y
lemma update_neq : forall f:func 'a 'b,x:'a,y:'b,z:'a.
x <> z -> update f x y z = f z
(* Abstraction definition axiom :
constant identity : func 'a 'a = (\ x:'a. x) *)
constant identity : func 'a 'a
axiom identity_def : forall x:'a. identity x = x
(* Abstraction definition axiom :
function compose (g:func 'b 'c) (f:func 'a 'b) : func 'a 'c =
(\ x:'a. g (f x)) *)
......@@ -40,36 +40,33 @@ module Func
axiom compose_def : forall g:func 'b 'c,f:func 'a 'b,x:'a.
compose g f x = g (f x)
function rcompose (f:func 'a 'b) (g:func 'b 'c) : func 'a 'c = compose g f
let lemma compose_associative (h:func 'c 'd) (g:func 'b 'c) (f:func 'a 'b) : unit
ensures { compose (compose h g) f = compose h (compose g f) }
=
assert { extensionalEqual (compose (compose h g) f) (compose h (compose g f)) }
let lemma identity_neutral (f:func 'a 'b) : unit
ensures { compose f identity = f }
ensures { compose identity f = f }
=
assert { extensionalEqual (compose f identity) f } ;
assert { extensionalEqual (compose identity f) f }
(* Abstraction definition axiom :
function const (x:'b) : func 'a 'b =
(\ z:'a.x) *)
function const (x: ~'b) : func 'a 'b
axiom const_def : forall x:'b,z:'a. const x z = x
let lemma const_compose_left (f:func 'a 'b) (x:'c) : unit
ensures { compose (const x) f = const x }
=
assert { extensionalEqual (const x) (compose (const x) f) }
let lemma const_compose_right (f:func 'a 'b) (x:'a) : unit
ensures { compose f (const x) = (const (f x):func 'c 'b) }
=
assert { extensionalEqual (const (f x) : func 'c 'b) (compose f (const x)) }
end
end
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../../bin/why3.opt
WHY3SHARE=../../../share
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
include $(WHY3SHARE)/Makefile.config
ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MLW=BacktrackArray Firstorder_symbol_impl ISet Firstorder_term_impl \
Firstorder_formula_impl Firstorder_formula_list_impl \
Firstorder_tableau_impl Unification FormulaTransformations \
Prover ProverMain ProverTest
BD=build
MLUTIL=$(BD)/Nat__Nat
MLTYPES=$(patsubst %,$(BD)/%__Types,$(MLW))
MLIMPL=$(patsubst %,$(BD)/%__Impl,$(MLW))
ML=$(MLUTIL) $(MLTYPES) $(MLIMPL)
CMX=$(patsubst %,%.cmx,$(ML))
CMI=$(patsubst %,%.cmi,$(ML))
OCAMLC=ocamlopt.opt
INCLUDES=-I $(BD) $(INCLUDE)
LIBS=nums.cmxa why3__BuiltIn.cmx int__Int.cmx array__Array.cmx
WHY3INC=-L .
MLFLAGS=
MLIFLAGS=
MLEXECFLAGS=
$(BD)/prover: $(CMX) $(BD)/Prover.ml
echo $(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
-o $(BD)/prover $<
# $(CMX) $(SRC)Prover.ml
%.cmx: %.ml
$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $*.ml
$(BD)/%__Types.ml: %.mlw
why3 $(WHY3INC) extract -D ocaml64 -o $(BD) $*.mlw -T Types
$(BD)/%__Impl.ml: %.mlw
why3 $(WHY3INC) extract -D ocaml64 -o $(BD) $*.mlw -T Impl
.PHONY: clean depend .depend
depend: .depend
.depend: Makefile $(patsubst %,%.ml,$(ML))
ocamldep.opt -I $(BD) $(patsubst %,%.ml,$(ML)) > .depend
include .depend
clean:
rm -f $(BD)/*.o $(BD)/*.cmi $(BD)/*.cmx
rm -f $(BD)/*__Types.ml $(BD)/*__Impl.ml
module Pred
use export HighOrd
use import Functions.Func
use import bool.Bool
predicate predExtensionalEqual (p q:pred 'a) =
forall x:'a. p x <-> q x
(* Assume extensionality of predicate. *)
axiom predicateExtensionality : forall p q:pred 'a.
predExtensionalEqual p q -> p = q
axiom predicateExtensionality "W:non_conservative_extension:N" :
forall p q:pred 'a. predExtensionalEqual p q -> p = q
(* Mainly for use in whyml *)
predicate evalp (p:pred 'a) (x:'a) = p x
(* Abstraction definition axiom :
pupdate (p:pred 'a) (x:'a) (y:bool) : pred 'a =
(\ z:'a. if x = z then y = True else p z) *)
function pupdate (p:pred 'a) (x:'a) (y:bool) : pred 'a
axiom pupdate_def : forall p:pred 'a,x:'a,y:bool,z:'a.
pupdate p x y z <-> if x = z then y = True else p z
lemma pupdate_eq : forall p:pred 'a,x:'a,y:bool.
pupdate p x y x <-> y = True
lemma pupdate_neq : forall p:pred 'a,x:'a,y:bool,z:'a.
x <> z -> pupdate p x y z <-> p z
(* Abstraction definition axiom :
function pcompose (p:pred 'b) (f:pred 'a 'b) : pred 'b =
(\ x:'a. p (f x)) *)
function pcompose (p:pred ~'b) (f:func ~'a 'b) : pred 'a
axiom pcompose_def : forall p:pred 'b,f:func 'a 'b,x:'a.
pcompose p f x <-> p (f x)
let lemma pcompose_associative (p:pred 'c) (g:func 'b 'c) (f:func 'a 'b) : unit
ensures { pcompose (pcompose p g) f = pcompose p (compose g f) }
=
assert { predExtensionalEqual (pcompose (pcompose p g) f) (pcompose p (compose g f)) }
let lemma identity_neutral (p:pred 'a) : unit
ensures { pcompose p identity = p }
=
assert { predExtensionalEqual (pcompose p identity) p }
(* Abstraction definition axiom :
constant pfalse : pred 'a = (\z:'a. false) *)
constant pfalse : pred ~'a
constant pfalse : pred 'a
axiom pfalse_def : forall x:'a. not(pfalse x)
(* Abstraction definition axiom :
constant ptrue : pred 'a = (\z:'a. true) *)
constant ptrue : pred ~'a
constant ptrue : pred 'a
axiom ptrue_def : forall x:'a. ptrue x
(*(* Abstraction definition axiom :
function const (x:'b) : func 'a 'b =
(\ z:'a.x) *)
function const (x: ~'b) : func ~'a ~'b
axiom const_def : forall x:'b,z:'a. const x z = x
let lemma const_compose_left (f:func 'a 'b) (x:'c) : unit
ensures { compose (const x) f = const x }
=
assert { extensionalEqual (const x) (compose (const x) f) }
let lemma const_compose_right (f:func 'a 'b) (x:'a) : unit
ensures { compose f (const x) = (const (f x):func 'c 'b) }
=
assert { extensionalEqual (const (f x) : func 'c 'b) (compose f (const x)) }*)
end
end
......@@ -443,7 +443,7 @@ let warn_dubious_axiom uc k p syms =
p.id_string
with Exit -> ()
let lab_w_conservative_extension_no = Ident.create_label "W:conservative_extension:N"
let lab_w_non_conservative_extension_no = Ident.create_label "W:non_conservative_extension:N"
let add_decl ?(warn=true) uc d =
check_decl_opacity d; (* we don't care about tasks *)
......@@ -456,7 +456,7 @@ let add_decl ?(warn=true) uc d =
| Dind (_, dl) -> List.fold_left add_ind uc dl
| Dprop ((k,pr,_) as p) ->
if warn &&
not (Slab.mem lab_w_conservative_extension_no pr.pr_name.id_label)
not (Slab.mem lab_w_non_conservative_extension_no pr.pr_name.id_label)
then warn_dubious_axiom uc k pr.pr_name d.d_syms;
add_prop uc p
......
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