...
 
Commits (65)
......@@ -417,12 +417,14 @@ PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUG_PYTHON = py_ast py_parser py_lexer py_main
PLUG_MICROC = mc_ast mc_parser mc_lexer mc_main
PLUG_CERT = cert_syntax cert_verif cert_transformations cert_register
PLUGINS = genequlin dimacs tptp python microc
PLUGINS = genequlin dimacs tptp python microc cert
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
PYTHONMODULES = $(addprefix plugins/python/, $(PLUG_PYTHON))
MICROCMODULES = $(addprefix plugins/microc/, $(PLUG_MICROC))
CERTMODULES = $(addprefix plugins/cert/, $(PLUG_CERT))
TPTPCMO = $(addsuffix .cmo, $(TPTPMODULES))
TPTPCMX = $(addsuffix .cmx, $(TPTPMODULES))
......@@ -433,6 +435,9 @@ PYTHONCMX = $(addsuffix .cmx, $(PYTHONMODULES))
MICROCCMO = $(addsuffix .cmo, $(MICROCMODULES))
MICROCCMX = $(addsuffix .cmx, $(MICROCMODULES))
CERTCMO = $(addsuffix .cmo, $(CERTMODULES))
CERTCMX = $(addsuffix .cmx, $(CERTMODULES))
ifeq (@enable_hypothesis_selection@,yes)
PLUG_TRANSFORM += hypothesis_selection
PLUGINS += hypothesis_selection
......@@ -446,13 +451,14 @@ endif
PLUGMODULES = $(addprefix plugins/parser/, $(PLUG_PARSER)) \
$(addprefix plugins/printer/, $(PLUG_PRINTER)) \
$(addprefix plugins/transform/, $(PLUG_TRANSFORM)) \
$(TPTPMODULES) $(PYTHONMODULES) $(MICROCMODULES)
$(TPTPMODULES) $(PYTHONMODULES) $(MICROCMODULES) $(CERTMODULES)
PLUGDEP = $(addsuffix .dep, $(PLUGMODULES))
PLUGCMO = $(addsuffix .cmo, $(PLUGMODULES))
PLUGCMX = $(addsuffix .cmx, $(PLUGMODULES))
PLUGDIRS = parser printer transform tptp python microc
PLUGDIRS = parser printer transform tptp python microc cert
PLUGINCLUDES = $(addprefix -I plugins/, $(PLUGDIRS))
$(PLUGDEP): DEPFLAGS += $(PLUGINCLUDES)
......@@ -489,6 +495,8 @@ lib/plugins/python.cmxs: $(PYTHONCMX)
lib/plugins/python.cmo: $(PYTHONCMO)
lib/plugins/microc.cmxs: $(MICROCCMX)
lib/plugins/microc.cmo: $(MICROCCMO)
lib/plugins/cert.cmxs: $(CERTCMX)
lib/plugins/cert.cmo: $(CERTCMO)
# depend and clean targets
......
......@@ -9,8 +9,8 @@ function morph Z.t : C.t
axiom morph_zero: morph Z.zero = C.zero
axiom morph_one: morph Z.one = C.one
axiom morph_add: forall z1 z2:Z.t. morph (Z.(+) z1 z2) = C.(+) (morph z1) (morph z2)
axiom morph_mul: forall z1 z2:Z.t. morph (Z.(*) z1 z2)
= C.(*) (morph z1) (morph z2)
axiom morph_mul: forall z1 z2:Z.t. morph (Z.( * ) z1 z2)
= C.( * ) (morph z1) (morph z2)
axiom morph_inv: forall z:Z.t. morph (Z.(-_) z) = C.(-_) (morph z)
val predicate eq0 (x:Z.t) ensures { result <-> x = Z.zero }
......@@ -26,7 +26,7 @@ function interp (x:t) (y:vars) : C.t =
match x with
| Var n -> y n
| Add x1 x2 -> C.(+) (interp x1 y) (interp x2 y)
| Mul x1 x2 -> C.(*) (interp x1 y) (interp x2 y)
| Mul x1 x2 -> C.( * ) (interp x1 y) (interp x2 y)
| Cst c -> morph c end
predicate eq (x1 x2:t) = forall y: vars. interp x1 y = interp x2 y
......@@ -39,12 +39,12 @@ type t' = list m (* sum of monomials *)
function mon (x:list int) (y:vars) : C.t =
match x with
| Nil -> C.one
| Cons x r -> C.(*) (y x) (mon r y) end
| Cons x r -> C.( * ) (y x) (mon r y) end
function interp' (x:t') (y:vars) : C.t =
match x with
| Nil -> C.zero
| Cons (M a m) r -> C.(+) (C.(*) (morph a) (mon m y)) (interp' r y) end
| Cons (M a m) r -> C.(+) (C.( * ) (morph a) (mon m y)) (interp' r y) end
predicate eq_mon (m1 m2: list int) = forall y: vars. mon m1 y = mon m2 y
predicate eq' (x1 x2: t') = forall y: vars. interp' x1 y = interp' x2 y
......@@ -53,7 +53,7 @@ use list.Append
use list.Length
let rec lemma mon_append (x1 x2: list int) (y:vars)
ensures { mon (x1 ++ x2) y = C.(*) (mon x1 y) (mon x2 y) }
ensures { mon (x1 ++ x2) y = C.( * ) (mon x1 y) (mon x2 y) }
variant { x1 }
=
match x1 with Nil -> () | Cons _ x -> mon_append x x2 y end
......@@ -72,12 +72,12 @@ let rec lemma interp_sum (x1 x2:t') (y:vars)
let ghost function append_mon (m1 m2:m)
ensures { forall y. interp' (Cons result Nil) y
= C.(*) (interp' (Cons m1 Nil) y) (interp' (Cons m2 Nil) y) }
= match m1,m2 with M a1 l1, M a2 l2 -> M (Z.(*) a1 a2) (l1 ++ l2) end
= C.( * ) (interp' (Cons m1 Nil) y) (interp' (Cons m2 Nil) y) }
= match m1,m2 with M a1 l1, M a2 l2 -> M (Z.( * ) a1 a2) (l1 ++ l2) end
let rec ghost function mul_mon (x:t') (mon:m) : t'
ensures { forall y.
interp' result y = C.(*) (interp' x y) (interp' (Cons mon Nil) y) }
interp' result y = C.( * ) (interp' x y) (interp' (Cons mon Nil) y) }
= match x with
| Nil -> Nil
| Cons m r ->
......@@ -87,7 +87,7 @@ let rec ghost function mul_mon (x:t') (mon:m) : t'
end
let rec ghost function mul_devel (x1 x2:t') : t'
ensures { forall y. interp' result y = C.(*) (interp' x1 y) (interp' x2 y) } =
ensures { forall y. interp' result y = C.( * ) (interp' x1 y) (interp' x2 y) } =
match x1 with
| Nil -> Nil
| Cons (M a m) r -> (mul_mon x2 (M a m)) ++ (mul_devel r x2)
......@@ -211,7 +211,7 @@ function id (x:int) : int = x
let predicate eq0_int (x:int) = x = 0
clone export UnitaryCommutativeRingDecision with type C.t = int, constant C.zero = zero, constant C.one = one, function C.(-_) = (-_), function C.(+) = (+), function C.(*) = (*), type Z.t = int, constant Z.zero = zero, constant Z.one = one, function Z.(-_) = (-_), function Z.(+) = (+), function Z.(*) = (*), function morph = id, goal morph_zero, goal morph_one, goal morph_add, goal morph_mul, goal morph_inv, val eq0 = eq0_int,
clone export UnitaryCommutativeRingDecision with type C.t = int, constant C.zero = zero, constant C.one = one, function C.(-_) = (-_), function C.(+) = (+), function C.( * ) = ( * ), type Z.t = int, constant Z.zero = zero, constant Z.one = one, function Z.(-_) = (-_), function Z.(+) = (+), function Z.( * ) = ( * ), function morph = id, goal morph_zero, goal morph_one, goal morph_add, goal morph_mul, goal morph_inv, val eq0 = eq0_int,
axiom . (* FIXME: replace with "goal" and prove *)
meta "compute_max_steps" 0x10000000
......@@ -227,10 +227,10 @@ type r
type a
function (+) a a : a
function (*) a a : a
function ( * ) a a : a
clone algebra.UnitaryCommutativeRing as R with type t = r, axiom .
clone algebra.Ring as A with type t = a, function (+) = (+), function (*) = (*), axiom .
clone algebra.Ring as A with type t = a, function (+) = (+), function ( * ) = ( * ), axiom .
constant one : a
constant zero : a = A.zero
axiom AUnitary : forall x:a. one * x = x * one = x
......@@ -243,7 +243,7 @@ val function ($) r a : a
axiom ExtDistSumA : forall r: r, x y: a. r $ (x + y) = r $ x + r $ y
axiom ExtDistSumR : forall r s: r, x: a. (R.(+) r s)$x = r$x + s$x
axiom AssocMulExt : forall r s: r, x: a. (R.(*) r s)$x = r$(s$x)
axiom AssocMulExt : forall r s: r, x: a. (R.( * ) r s)$x = r$(s$x)
axiom UnitExt : forall x: a. R.one $ x = x
axiom CommMulExt : forall r: r, x y: a. r$(x*y) = (r$x)*y = x*(r$y)
......@@ -273,7 +273,7 @@ val function aplus a a : a
val function atimes a a : a
val function aopp a : a
clone export AssocAlgebra with type r = r, type a = a, constant one = aone, constant A.zero = azero, constant R.zero = rzero, constant R.one = rone, function R.(+) = rplus, function R.(*) = rtimes, function R.(-_) = ropp, function (+) = aplus, function (*) = atimes, function A.(-_) = aopp, axiom .
clone export AssocAlgebra with type r = r, type a = a, constant one = aone, constant A.zero = azero, constant R.zero = rzero, constant R.one = rone, function R.(+) = rplus, function R.( * ) = rtimes, function R.(-_) = ropp, function (+) = aplus, function ( * ) = atimes, function A.(-_) = aopp, axiom .
(*axiom azero_def: azero = A.zero*) (* FIXME *)
......@@ -465,7 +465,7 @@ let predicate eq0_int (x:int) = x=0
let function ($$) (x y:int) :int = x * y
clone export AssocAlgebraDecision with type r = int, type a = int, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = (*), val azero = Int.zero, val aone = Int.one, val aplus = (+), val aopp = (-_), val atimes = (*), val ($) = ($$), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc,
clone export AssocAlgebraDecision with type r = int, type a = int, val rzero = Int.zero, val rone = Int.one, val rplus = (+), val ropp = (-_), val rtimes = ( * ), val azero = Int.zero, val aone = Int.one, val aplus = (+), val aopp = (-_), val atimes = ( * ), val ($) = ($$), goal AUnitary, goal ANonTrivial, goal ExtDistSumA, goal ExtDistSumR, goal AssocMulExt, goal UnitExt, goal CommMulExt, val eq0 = eq0_int, goal A.MulAssoc.Assoc, goal A.Unit_def_l, goal A.Unit_def_r, goal A.Comm, goal A.Assoc,
axiom . (* FIXME: replace with "goal" and prove *)
......
open Why3
open Cert_syntax
open Cert_transformations
open Cert_verif
(** Certified transformations *)
let checker_ctrans = checker_ctrans check_certif ctask_equal
let assumption_trans = checker_ctrans assumption
let trivial_trans = checker_ctrans trivial
let exfalso_trans = checker_ctrans exfalso
let intros_trans = checker_ctrans intros
let intuition_trans = checker_ctrans intuition
let swap_trans where = checker_ctrans (swap where)
let revert_trans ls = checker_ctrans (revert ls)
let intro_trans where = checker_ctrans (intro where)
let left_trans where = checker_ctrans (dir Left where)
let right_trans where = checker_ctrans (dir Right where)
let split_trans where = checker_ctrans (split_logic where)
let instantiate_trans t what = checker_ctrans (inst t what)
let assert_trans t = checker_ctrans (cut t)
let case_trans t = checker_ctrans (case t)
let rewrite_trans g rev where = checker_ctrans (rewrite g rev where)
let clear_trans l = checker_ctrans (clear l)
let pose_trans name t = checker_ctrans (pose name t)
(** Register certified transformations *)
let () =
let open Args_wrapper in let open Trans in
register_transform_l "assumption_cert" (store assumption_trans)
~desc:"A certified version of coq tactic [assumption]";
register_transform_l "trivial_cert" (store trivial_trans)
~desc:"A certified version of (simplified) coq tactic [trivial]";
register_transform_l "exfalso_cert" (store exfalso_trans)
~desc:"A certified version of coq tactic [exfalso]";
register_transform_l "intros_cert" (store intros_trans)
~desc:"A certified version of coq tactic [intros]";
register_transform_l "intuition_cert" (store intuition_trans)
~desc:"A certified version of (simplified) coq tactic [intuition]";
wrap_and_register ~desc:"A certified transformation that negates \
and swaps an hypothesis from the context to the goal]"
"swap_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (swap_trans where));
wrap_and_register ~desc:"A certified transformation that generalizes a variable in the goal"
"revert_cert" (Tlsymbol (Ttrans_l))
(fun ls -> store (revert_trans ls));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [intro]"
"intro_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (intro_trans where));
wrap_and_register ~desc:"A certified version of coq tactic [left]"
"left_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (left_trans where));
wrap_and_register ~desc:"A certified version of coq tactic [right]"
"right_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (right_trans where));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [split]"
"split_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (split_trans where));
wrap_and_register ~desc:"A certified version of transformation instantiate"
"instantiate_cert" (Tterm (Topt ("in", Tprsymbol Ttrans_l)))
(fun t_inst where -> store (instantiate_trans t_inst where));
wrap_and_register ~desc:"A certified version of transformation rewrite"
"rewrite_cert" (Toptbool ("<-", (Tprsymbol (Topt ("in", Tprsymbol (Ttrans_l))))))
(fun rev g where -> store (rewrite_trans g rev where));
wrap_and_register ~desc:"A certified version of transformation assert"
"assert_cert" (Tformula Ttrans_l)
(fun t -> store (assert_trans t));
wrap_and_register ~desc:"A certified version of transformation case"
"case_cert" (Tformula Ttrans_l)
(fun t -> store (case_trans t));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [clear]"
"clear_cert" (Tprlist Ttrans_l)
(fun l -> store (clear_trans l));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [pose]"
"pose_cert" (Tstring (Tformula Ttrans_l))
(fun name t -> store (pose_trans name t))
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
predicate a
predicate b
predicate c
predicate d
predicate e
predicate f
axiom A : a
axiom B : b
predicate p (x : bool)
goal G1 : a /\ b
goal G2 : (a /\ b) /\ (a /\ a /\ a /\ b)
goal G3 : (b /\ a) /\ ( (a /\ a) /\ c)
goal G4 : a /\ (b \/ d)
goal G5 : (a \/ c) /\ (d \/ b)
goal G6 : a /\ (c \/ d)
goal G7 : (a /\ (d \/ c) ) \/ ( ((a /\ b) /\ ((b /\ (d \/ e \/ a)) \/d)) \/ (a /\ c) )
goal G8 : ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) /\ ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))))
goal G9 : c /\ (d \/ f) <-> (c /\ d) \/ (c /\ f)
goal G10 : c -> d
goal G11 : a /\ (d -> d)
goal G12 : (c <-> a) -> (d \/ c)
goal G13 : (c <-> d) -> c -> d
goal G14 : (d <-> c) -> c -> d
goal G15 : (a -> b -> d <-> c) -> c -> d
goal G16 : d \/ c -> c
goal G17 : (d <-> a) -> d
goal G18 : a -> d -> b -> c -> a -> d
goal G19 : forall x. (forall u. u <-> a) -> (x <-> x)
goal G20 : exists x : bool. p x -> (forall y. p y)
goal G21 : true
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file>
<path name=".."/>
<path name="tests.mlw"/>
<theory name="Top">
<goal name="G1" proved="true">
<transf name="assert" arg1="(forall x. p x)">
<goal name="G1.0" expl="asserted formula">
</goal>
<goal name="G1.1">
</goal>
</transf>
<transf name="case_cert" arg1="true">
<goal name="G1.0">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G1.1">
<proof prover="0" obsolete="true"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G2" proved="true">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G3">
<transf name="intuition_cert" >
<goal name="G3.0">
<transf name="assert_cert" arg1="true">
<goal name="G3.0.0" proved="true">
<transf name="trivial_cert" proved="true" >
</transf>
</goal>
<goal name="G3.0.1">
<transf name="exfalso_cert" >
<goal name="G3.0.1.0">
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G4" proved="true">
<transf name="case_cert" arg1="true">
<goal name="G4.0">
</goal>
<goal name="G4.1">
</goal>
</transf>
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G5" proved="true">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G6">
<transf name="intuition_cert" >
<goal name="G6.0">
</goal>
</transf>
</goal>
<goal name="G7" proved="true">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G8" proved="true">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G9">
<transf name="intuition_cert" >
<goal name="G9.0">
</goal>
<goal name="G9.1">
</goal>
<goal name="G9.2">
</goal>
</transf>
</goal>
<goal name="G10">
<transf name="intro_cert" >
<goal name="G10.0">
</goal>
</transf>
</goal>
<goal name="G11" proved="true">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G12" proved="true">
<transf name="intro_cert" proved="true" >
<goal name="G12.0" proved="true">
<transf name="rewrite_cert" proved="true" arg1="H">
<goal name="G12.0.0" proved="true">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G13" proved="true">
<transf name="intros_cert" proved="true" >
<goal name="G13.0" proved="true">
<transf name="rewrite_cert" proved="true" arg1="H1" arg2="in" arg3="H">
<goal name="G13.0.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G14" proved="true">
<transf name="intros_cert" proved="true" >
<goal name="G14.0" proved="true">
<transf name="rewrite_cert" proved="true" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G14.0.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
<transf name="trivial_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G15" proved="true">
<transf name="intros_cert" proved="true" >
<goal name="G15.0" proved="true">
<transf name="rewrite" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G15.0.0">
</goal>
<goal name="G15.0.1" expl="rewrite premises">
</goal>
<goal name="G15.0.2" expl="rewrite premises">
</goal>
</transf>
<transf name="rewrite_cert" proved="true" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G15.0.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G15.0.1" expl="rewrite premises" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G15.0.2" expl="rewrite premises" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G16">
<transf name="intro_cert" >
<goal name="G16.0">
<transf name="split_cert" arg1="in" arg2="H">
<goal name="G16.0.0">
</goal>
<goal name="G16.0.1">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G17">
<transf name="intro_cert" >
<goal name="G17.0">
<transf name="split_cert" arg1="in" arg2="H">
<goal name="G17.0.0">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G18" proved="true">
<transf name="intros_cert" proved="true" >
<goal name="G18.0" proved="true">
<transf name="clear_cert" proved="true" arg1="H4,H2,H1,H,A,B">
<goal name="G18.0.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G19">
<transf name="introduce_premises" >
<goal name="G19.0">
<transf name="revert_cert" arg1="x">
<goal name="G19.0.0">
</goal>
</transf>
<transf name="rewrite" arg1="H">
<goal name="G19.0.0">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G20" proved="true">
<transf name="case_cert" proved="true" arg1="(exists x. not p x)">
<goal name="G20.0" proved="true">
<transf name="intro_cert" proved="true" arg1="in" arg2="H">
<goal name="G20.0.0" proved="true">
<transf name="instantiate_cert" proved="true" arg1="x">
<goal name="G20.0.0.0" proved="true">
<transf name="intro_cert" proved="true" >
<goal name="G20.0.0.0.0" proved="true">
<transf name="swap_cert" proved="true" arg1="in" arg2="H2">
<goal name="G20.0.0.0.0.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G20.1" proved="true">
<transf name="instantiate_cert" proved="true" arg1="True">
<goal name="G20.1.0" proved="true">
<transf name="intros_cert" proved="true" >
<goal name="G20.1.0.0" proved="true">
<transf name="swap_cert" proved="true" >
<goal name="G20.1.0.0.0" proved="true">
<transf name="swap_cert" proved="true" arg1="in" arg2="H3">
<goal name="G20.1.0.0.0.0" proved="true">
<transf name="instantiate_cert" proved="true" arg1="y">
<goal name="G20.1.0.0.0.0.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G21">
<transf name="pose_cert" arg1="hh" arg2="true">
<goal name="G21.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -266,9 +266,9 @@ let replace rev f1 f2 t =
- Else call recursively on subterms of t *)
(* If a substitution s is found then new premises are computed as e -> s.e *)
let replace_subst lp lv llet f1 f2 withed_terms t =
(* is_replced is common to the whole execution of replace_subst. Once an
(* is_replaced is common to the whole execution of replace_subst. Once an
occurence is found, it changes to Some (s) so that only one instanciation
is rewrritten during execution *)
is rewritten during execution *)
let rec replace is_replaced f1 f2 t : _ * Term.term =
match is_replaced with
| Some(subst_ty,subst) ->
......
......@@ -154,6 +154,7 @@ let collect_lsymbol s (d: decl) =
used in the declaration d. *)
let depends dep d =
let new_set = collect_lsymbol Sls.empty d in
(* not (Sls.disjoint dep new_set) *)
if Sls.equal (Sls.inter dep new_set) Sls.empty then
false
else
......
......@@ -71,6 +71,9 @@ let fold_product_l f acc ll =
let flatten_rev fl =
List.fold_left (fun acc l -> List.rev_append l acc) [] fl
let rev_flatten fl =
List.fold_left (fun acc l -> l @ acc) [] fl
let part cmp l =
let l = List.stable_sort cmp l in
match l with
......
......@@ -43,6 +43,8 @@ val fold_product_l : ('a -> 'b list -> 'a) -> 'a -> 'b list list -> 'a
val flatten_rev : 'a list list -> 'a list
val rev_flatten : 'a list list -> 'a list
val part : ('a -> 'a -> int) -> 'a list -> 'a list list
(** [part cmp l] returns the list of the congruence classes with
respect to [cmp]. They are returned in reverse order *)
......
predicate a
predicate b
predicate c
axiom A : a
axiom B : b
goal G : a
goal G1 : a /\ b
goal G2 : a /\ c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<file>
<path name=".."/>
<path name="test1.mlw"/>
<theory name="Top">
<goal name="G" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G1" proved="true">
<transf name="split_cert" proved="true" >
<goal name="G1.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G1.1" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="G2">
<transf name="split_cert" >
<goal name="G2.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G2.1">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>