Commit b5b2add1 authored by François Bobot's avatar François Bobot

Merge branch 'computer_division_for_master' into 'master'

Computer division for master

See merge request !5
parents 116df251 dd3125e9
......@@ -1015,6 +1015,8 @@ COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
endif
COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT)
%.vo: %.v
......@@ -1063,9 +1065,11 @@ drivers/coq-realizations.aux: Makefile
echo 'theory ieee_float.'"$$f"' meta "realized_theory" "ieee_float.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FOR_DRIVER_FILES); do \
echo 'theory for_driver.'"$$f"' meta "realized_theory" "for_driver.'"$$f"'", "" end'; done; \
) > $@
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-bv update-coq-ieee_float
update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option update-coq-fp update-coq-bv update-coq-ieee_float update-coq-for-drivers
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/int.mlw
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T int.$$f -o $(GENERATED_PREFIX_COQ)/int/; done
......@@ -1094,6 +1098,9 @@ update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdl
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/bv.mlw
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T bv.$$f -o $(GENERATED_PREFIX_COQ)/bv/; done
update-coq-for-drivers: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/for_drivers.why
for f in $(COQLIBS_FOR_DRIVERS_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T for_drivers.$$f -o $(GENERATED_PREFIX_COQ)/for_drivers/; done
update-coq-ieee_float: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux stdlib/ieee_float.mlw
for f in $(COQLIBS_IEEEFLOAT_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L stdlib -D drivers/coq-realize.drv -T ieee_float.$$f -o $(GENERATED_PREFIX_COQ)/ieee_float/; done
......
......@@ -82,10 +82,10 @@ valid_goals () {
test -d $1 || exit 1
for f in $1/*.mlw; do
printf " $f... "
if ! $pgm -t 15 -P alt-ergo $f > /dev/null 2>&1; then
if ! $pgm -t 15 -P alt-ergo $2 $f > /dev/null 2>&1; then
echo "FAILED!"
echo "$pgm -t 15 -P alt-ergo $f"
$pgm -t 15 -P alt-ergo $f
echo "$pgm -t 15 -P alt-ergo $2 $f"
$pgm -t 15 -P alt-ergo $2 $f
exit 1
fi
echo "ok"
......@@ -308,6 +308,10 @@ echo "=== Checking valid goals ==="
valid_goals bench/valid
echo ""
echo "=== Checking splitted valid goals ==="
valid_goals bench/valid/split_vc "-a split_vc"
echo ""
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""
......
../../examples/mccarthy.mlw
\ No newline at end of file
(** {1 McCarthy's "91" function}
authors: Jean-Christophe Filliâtre, Martin Clochard, Claude Marché
witness: Andrei Paskevich
*)
module McCarthy91
use int.Int
(** {2 Specification} *)
function spec (x: int) : int = if x <= 100 then 91 else x-10
(** {2 traditional recursive implementation} *)
let rec f91 (n:int) : int variant { 101-n }
ensures { result = spec n }
= if n <= 100 then
f91 (f91 (n + 11))
else
n - 10
(** {2 non-recursive implementation using a while loop} *)
use ref.Ref
use int.Iter
let f91_nonrec (n0: int) ensures { result = spec n0 }
= let e = ref 1 in
let n = ref n0 in
while !e > 0 do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
variant { 101 - !n + 10 * !e, !e }
if !n > 100 then begin
n := !n - 10;
e := !e - 1
end else begin
n := !n + 11;
e := !e + 1
end
done;
!n
(** {2 irrelevance of control flow}
We use a 'morally' irrelevant control flow from a recursive function
to ease proof (the recursive structure does not contribute to the
program execution). This is a technique for proving derecursified
programs. See [verifythis_2016_tree_traversal] for a more
complex example. *)
exception Stop
let f91_pseudorec (n0:int) : int
ensures { result = spec n0 }
= let e = ref 1 in
let n = ref n0 in
let bloc () : unit
requires { !e >= 0 }
ensures { !(old e) > 0 }
ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1
else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
= if not (!e > 0) then raise Stop;
if !n > 100 then begin
n := !n - 10;
e := !e - 1
end else begin
n := !n + 11;
e := !e + 1
end
in
let rec aux () : unit
requires { !e > 0 }
variant { 101 - !n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
raises { Stop -> false }
= let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd
with Stop -> !n end
end
module McCarthyWithCoroutines
use int.Int
use ref.Ref
function spec (x: int) : int = if x <= 100 then 91 else x-10
(** {2 Variant using a general 'ghost coroutine' approach}
Assume we want to prove the imperative code:
{h <pre>
e <- 1; r <- n;
loop
if r > 100 { r <- r - 10; e <- e - 1; if e = 0 break }
else { r <- r + 11; e <- e + 1 }
end-loop
</pre>}
we annotate the various program points:
{h <pre>
{ 0 } e <- 1;
{ 1 } r <- n;
loop
{ 2 } if r > 100 then { 3 } r <- r - 10; { 4 } e <- e - 1; { 5 } if e=0 then break;
else { 6 } r <- r + 11; { 7 } e <- e + 1;
end-loop
{ 8 }
</pre>}
we define the small-step semantics of this code by the following [step] function
*)
val pc : ref int
val n : ref int
val e : ref int
val r : ref int
val step () : unit
requires { 0 <= !pc < 8 }
writes { pc, e, r }
ensures { old !pc = 0 -> !pc = 1 /\ !e = 1 /\ !r = old !r }
ensures { old !pc = 1 -> !pc = 2 /\ !e = old !e /\ !r = !n }
ensures { old !pc = 2 /\ old !r > 100 -> !pc = 3 /\ !e = old !e /\ !r = old !r }
ensures { old !pc = 2 /\ old !r <= 100 -> !pc = 6 /\ !e = old !e /\ !r = old !r }
ensures { old !pc = 3 -> !pc = 4 /\ !e = old !e /\ !r = old !r - 10 }
ensures { old !pc = 4 -> !pc = 5 /\ !e = old !e - 1 /\ !r = old !r }
ensures { old !pc = 5 /\ old !e = 0 -> !pc = 8 /\ !e = old !e /\ !r = old !r }
ensures { old !pc = 5 /\ old !e <> 0 -> !pc = 2 /\ !e = old !e /\ !r = old !r }
ensures { old !pc = 6 -> !pc = 7 /\ !e = old !e /\ !r = old !r + 11 }
ensures { old !pc = 7 -> !pc = 2 /\ !e = old !e + 1 /\ !r = old !r }
let rec aux1 () : unit
requires { !pc = 2 /\ !e > 0 }
variant { 101 - !r }
ensures { !pc = 5 /\ !r = spec(old !r) /\ !e = old !e - 1 }
= step (); (* execution of 'if r > 100' *)
if !pc = 3 then begin
step (); (* assignment r <- r - 10 *)
step (); (* assignment e <- e - 1 *)
end
else begin
step (); (* assignment r <- r + 11 *)
step (); (* assignment e <- e + 1 *)
aux1 ();
step (); (* 'if e=0' must be false *)
aux1 ()
end
let mccarthy1 ()
requires { !pc = 0 /\ !n >= 0 }
ensures { !pc = 8 /\ !r = spec !n }
= step (); (* assignment e <- 1 *)
step (); (* assignment r <- n *)
aux1 (); (* loop *)
step() (* loop exit *)
(** {2 a variant with not-so-small steps}
we annotate the important program points:
{h <pre>
{ 0 } e <- 1;
r <- n;
loop
{ 1 } if r > 100 { r <- r - 10; e <- e - 1; { 2 } if e = 0 break; }
else { r <- r + 11; e <- e + 1; }
end-loop
end-while
{ 3 }
return r
</pre>}
we define the not-so-small-step semantics of this code by the following [next] function
*)
val next () : unit
requires { 0 <= !pc < 3 }
writes { pc, e, r }
ensures { old !pc = 0 -> !pc = 1 /\ !e = 1 /\ !r = !n }
ensures { old !pc = 1 /\ old !r > 100 ->
!pc = 2 /\ !r = old !r - 10 /\ !e = old !e - 1 }
ensures { old !pc = 1 /\ old !r <= 100 ->
!pc = 1 /\ !r = old !r + 11 /\ !e = old !e + 1 }
ensures { old !pc = 2 /\ old !e = 0 -> !pc = 3 /\ !r = old !r /\ !e = old !e }
ensures { old !pc = 2 /\ old !e <> 0 -> !pc = 1 /\ !r = old !r /\ !e = old !e }
(* [aux2] performs as may loop iterations as needed so as to reach program point 2
from program point 1 *)
let rec aux2 () : unit
requires { !pc = 1 /\ !e > 0 }
variant { 101 - !r }
ensures { !pc = 2 /\ !r = spec(old !r) /\ !e = old !e - 1 }
= next ();
if !pc <> 2 then begin aux2 (); next (); aux2 () end
let mccarthy2 ()
requires { !pc = 0 /\ !n >= 0 }
ensures { !pc = 3 /\ !r = spec !n }
= next (); (* assignments e <- 1; r <- n *)
aux2 (); (* loop *)
next ()
end
module McCarthy91Mach
use int.Int
use mach.int.Int63
function spec (x: int) : int = if x <= 100 then 91 else x-10
let rec f91 (n: int63) : int63
variant { 101 - n }
ensures { result = spec n }
= if n <= 100 then
f91 (f91 (n + 11))
else
n - 10
use mach.peano.Peano
use mach.int.Refint63
use int.Iter
let f91_nonrec (n0: int63) : int63
ensures { result = spec n0 }
= let e = ref one in
let n = ref n0 in
while gt !e zero do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
variant { 101 - !n + 10 * !e, !e:int }
if !n > 100 then begin
n := !n - 10;
e := pred !e
end else begin
assert { spec !n = spec (spec (!n + 11)) };
n := !n + 11;
e := succ !e
end
done;
!n
exception Stop
let f91_pseudorec (n0: int63) : int63
ensures { result = spec n0 }
= let e = ref one in
let n = ref n0 in
let bloc () : unit
requires { !e >= 0 }
ensures { !(old e) > 0 }
ensures { if !(old n) > 100 then !n = !(old n) - 10 /\ !e = !(old e) - 1
else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
= if not (gt !e zero) then raise Stop;
if !n > 100 then begin
n := !n - 10;
e := pred !e
end else begin
n := !n + 11;
e := succ !e
end
in
let rec aux () : unit
requires { !e > 0 }
variant { 101 - !n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
raises { Stop -> false }
= let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd
with Stop -> !n end
end
......@@ -98,14 +98,7 @@ end
theory int.ComputerDivision
prelude "logic comp_div: int, int -> int"
prelude "axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y"
prelude "logic comp_mod: int, int -> int"
prelude "axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y"
syntax function div "comp_div(%1,%2)"
syntax function mod "comp_mod(%1,%2)"
use for_drivers.ComputerOfEuclideanDivision
end
......
......@@ -242,6 +242,7 @@ module McCarthy91Mach
n := !n - 10;
e := pred !e
end else begin
assert { spec !n = spec (spec (!n + 11)) };
n := !n + 11;
e := succ !e
end
......
......@@ -3,17 +3,18 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw" proved="true">
<theory name="McCarthy91" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00" steps="31"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="31"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.29" steps="517"/></proof>
<proof prover="1"><result status="valid" time="0.29" steps="517"/></proof>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.01" steps="49"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="49"/></proof>
</goal>
</theory>
<theory name="McCarthyWithCoroutines" proved="true">
......@@ -32,13 +33,41 @@
</theory>
<theory name="McCarthy91Mach" proved="true">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="1067"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.07" steps="1067"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1"><result status="valid" time="6.06" steps="12891"/></proof>
<transf name="split_vc" proved="true" >
<goal name="VC f91_nonrec.0" expl="loop invariant init" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="14"/></proof>
</goal>
<goal name="VC f91_nonrec.1" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="26"/></proof>
</goal>
<goal name="VC f91_nonrec.2" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="32"/></proof>
</goal>
<goal name="VC f91_nonrec.3" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="200"/></proof>
</goal>
<goal name="VC f91_nonrec.4" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="100"/></proof>
</goal>
<goal name="VC f91_nonrec.5" expl="integer overflow" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC f91_nonrec.6" expl="loop variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="34"/></proof>
</goal>
<goal name="VC f91_nonrec.7" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="274"/></proof>
</goal>
<goal name="VC f91_nonrec.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00" steps="20"/></proof>
</goal>
</transf>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="432"/></proof>
<proof prover="1" timelimit="5"><result status="valid" time="0.08" steps="432"/></proof>
</goal>
</theory>
</file>
......
......@@ -53,4 +53,7 @@ theory ComputerDivTest
goal smoke5 : div_m1_m2 = -1
goal smoke6 : mod_m1_m2 = 1
end
\ No newline at end of file
goal div_pos_neg: forall x y. x>=0 -> y<0 -> div x y <= 0
end
......@@ -3,7 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="2" steplimit="0" memlimit="4000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -570,6 +572,10 @@
<proof prover="25"><result status="unknown" time="0.14"/></proof>
<proof prover="26"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="div_pos_neg" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
</file>
</why3session>
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Lemma on_pos_euclidean_is_div:
forall n d, (int.EuclideanDivision.div n (Zpos d)) = Zdiv n (Zpos d).
intros n d.
unfold EuclideanDivision.div.
assert (0 < Z.pos d)%Z by reflexivity.
destruct (Z.mod_pos_bound n (Zpos d) H).
case (Z_le_dec 0 (n mod (Zpos d))); intros H2.
* reflexivity.
* destruct (H2 H0).
Qed.
(* Why3 goal *)
Lemma cdiv_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d)))) /\
(((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z
d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n
(-d)%Z))%Z))) /\ ((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z
(-d)%Z)))))).
intros n d.
destruct d as [|d|d]; destruct n as [|n|n]; intuition (try contradiction; try discriminate; auto).
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
rewrite Z.mul_1_l.
reflexivity.
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
destruct (Z.pos n / Z.pos d)%Z;reflexivity.
Qed.
(* Why3 goal *)
Lemma cmod_cases : forall (n:Z) (d:Z), ((0%Z <= n)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d)))) /\
(((n <= 0%Z)%Z -> ((0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
d))%Z))) /\ (((0%Z <= n)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z)))) /\
((n <= 0%Z)%Z -> ((d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z
(-d)%Z))%Z))))).
intros n d.
unfold int.EuclideanDivision.mod1.
SearchAbout Z.rem Z.quot.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
assert (H:= Z.quot_rem' n d).
omega.
rewrite H.
assert (H2:=cdiv_cases n d).
intuition.
+ rewrite H1.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_r.
omega.
+ rewrite H1.
rewrite Z.mul_opp_r.
rewrite Z.mul_opp_l.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_l.
omega.
Qed.
......@@ -55,6 +55,8 @@ val ls_hash : lsymbol -> int
val create_lsymbol : ?constr:int -> preid -> ty list -> ty option -> lsymbol
val create_fsymbol : ?constr:int -> preid -> ty list -> ty -> lsymbol
(** ~constr is the number of constructors of the type in which the
symbol is a constructor otherwise it must be the default 0. *)
val create_psymbol : preid -> ty list -> lsymbol
......
......@@ -30,6 +30,7 @@ type driver = {
drv_transform : string list;
drv_prelude : prelude;
drv_thprelude : prelude_map;
drv_thuse : (theory * theory) Mid.t;
drv_blacklist : string list;
drv_meta : (theory * Stdecl.t) Mid.t;
drv_res_parser : prover_result_parser;
......@@ -118,6 +119,7 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
let thprelude = ref Mid.empty in
let meta = ref Mid.empty in
let qualid = ref [] in
let thuse = ref Mid.empty in
let find_pr th (loc,q) = try ns_find_pr th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
......@@ -138,34 +140,43 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
let s = try snd (Mid.find th.th_name !m) with Not_found -> Stdecl.empty in
m := Mid.add th.th_name (th, Stdecl.add td s) !m
in
let add_local th = function
(* th_uc is the theory built with the uses forced by the driver *)
let add_local th th_uc = function
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
thprelude := Mid.add th.th_name (s::l) !thprelude;
th_uc
| Rsyntaxts (q,s,b) ->
let td = syntax_type (find_ts th q) s b in
add_meta th td meta
add_meta th td meta;
th_uc
| Rsyntaxfs (q,s,b) ->
let td = syntax_logic (find_fs th q) s b in
add_meta th td meta
add_meta th td meta;
th_uc
| Rsyntaxps (q,s,b) ->
let td = syntax_logic (find_ps th q) s b in
add_meta th td meta
add_meta th td meta;
th_uc
| Rremovepr (q) ->
let td = remove_prop (find_pr th q) in
add_meta th td meta
add_meta th td meta;
th_uc
| Rremoveall ->
let it key _ = match (Mid.find key th.th_known).d_node with
| Dprop (_,symb,_) -> add_meta th (remove_prop symb) meta
| _ -> ()
in
Mid.iter it th.th_local
Mid.iter it th.th_local;
th_uc
| Rconverter (q,s,b) ->
let cs = syntax_converter (find_ls th q) s b in
add_meta th cs meta
add_meta th cs meta;
th_uc
| Rliteral (q,s,b) ->
let cs = syntax_literal (find_ts th q) s b in
add_meta th cs meta
add_meta th cs meta;
th_uc
| Rmeta (s,al) ->
let rec ty_of_pty = function
| PTyvar x ->
......@@ -190,14 +201,22 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
in
let m = lookup_meta s in
let td = create_meta m (List.map convert al) in
add_meta th td meta
add_meta th td meta;
th_uc
| Ruse (loc,q) ->
let file, th = Lists.chop_last q in
let th = Loc.try3 ~loc Env.read_theory env file th in
Theory.use_export th_uc th
in
let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in
let add_local th th_uc (loc,rule) = Loc.try2 ~loc add_local th th_uc rule in
let add_theory { thr_name = (loc,q); thr_rules = trl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let f,id = Lists.chop_last q in
let th = Loc.try3 ~loc Env.read_theory env f id in
let th_uc = Theory.create_theory (Ident.id_fresh ~loc ("driver export for "^th.th_name.id_string)) in
qualid := q;
List.iter (add_local th) trl
let th_uc' = List.fold_left (add_local th) th_uc trl in
if th_uc != th_uc' then
thuse := Mid.add th.th_name (th, Theory.close_theory th_uc') !thuse
in
List.iter add_theory f.f_rules;
List.iter (fun f -> List.iter add_theory (load_file f).f_rules) extra_files;
......@@ -220,6 +239,7 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
prp_model_parser = Model_parser.lookup_model_parser !model_parser
};
drv_tag = !driver_tag;
drv_thuse = !thuse;
}
let syntax_map drv =
......@@ -265,20 +285,35 @@ let call_on_buffer ~command ~limit ~gen_new_file ?inplace ~filename
exception NoPrinter
let update_task = let ht = Hint.create 5 in fun drv ->
let update task0 =
Mid.fold (fun _ (th,tdms) task ->