Commit 7ac40586 authored by MARCHE Claude's avatar MARCHE Claude

Time bomb with pairing defused (some sessions still need update)

parent 0793682b
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......@@ -39,7 +39,7 @@
name="l_false"
locfile="../fsetint.why"
loclnum="5" loccnumb="9" loccnume="16"
sum="19aa670ee65262a5273fbff8b07c2dfb"
sum="088ef7be07afff4f21ab9fbe516655fb"
proved="false"
expanded="true"
shape="f">
......@@ -103,7 +103,7 @@
name="mem_integer"
locfile="../fsetint.why"
loclnum="13" loccnumb="8" loccnume="19"
sum="9ffa692caa04cddd289b902664e6d758"
sum="7000a15f6e25f597fcc465bb02287359"
proved="false"
expanded="true"
shape="amemV0aintegerF">
......@@ -160,7 +160,7 @@
name="foo"
locfile="../fsetint.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="98f6e78fbd3f6e82548f42970ed744cc"
sum="7406e1d12a6379e6084dccd0fe4bab2a"
proved="false"
expanded="true"
shape="f">
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......@@ -99,7 +99,7 @@
sum="38bd50e1a687c7a7c325602b465c4535"
proved="true"
expanded="true"
shape="ainfix =agetasetV4V0V3V2V1Iainfix =agetV4V2V1Iainfix =V2V0NFF">
shape="ainfix =agetasetV4V0V3V2V1Iainfix =agetV4V2V1INainfix =V2V0FF">
<proof
prover="0"
timelimit="10"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......@@ -34,7 +34,7 @@
sum="52b6f59c45a8b8a73a77412fcd2fe40a"
proved="true"
expanded="true"
shape="ainfix =aTrueaFalseN">
shape="Nainfix =aTrueaFalse">
<proof
prover="0"
timelimit="10"
......@@ -116,7 +116,7 @@
sum="748209c7ed2ad6f059044132d8222014"
proved="true"
expanded="true"
shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
shape="fINainfix =V2V0ANainfix =V1V2ANainfix =V0V1F">
<proof
prover="0"
timelimit="10"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......@@ -376,7 +376,7 @@
sum="f636bb6e2df3c1171fca9a806d47a575"
proved="true"
expanded="true"
shape="ainfix =afrom_intafloorV0V0NIainfix &lt;afloorV0aceilV0F">
shape="Nainfix =afrom_intafloorV0V0Iainfix &lt;afloorV0aceilV0F">
<proof
prover="0"
timelimit="10"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......@@ -23,7 +23,7 @@
sum="9c086128d576bac08b0bb260172084f2"
proved="false"
expanded="true"
shape="ainfix &lt;=iainfix &gt;=V0c42ainfix +V0c3c0c50F">
shape="ainfix &lt;=ic0ainfix +V0c3ainfix &gt;=V0c42c50F">
<label
name="expl:VC for f"/>
<proof
......@@ -43,7 +43,7 @@
sum="9c086128d576bac08b0bb260172084f2"
proved="false"
expanded="true"
shape="ainfix &lt;=iainfix &gt;=V0c42ainfix +V0c3c0c50F">
shape="ainfix &lt;=ic0ainfix +V0c3ainfix &gt;=V0c42c50F">
<label
name="expl:VC for f_no_lab"/>
<proof
......@@ -63,7 +63,7 @@
sum="6866337a86e86f8b1444d48a89e38adf"
proved="false"
expanded="true"
shape="iainfix &gt;=V1c42ainfix &lt;=ainfix +V1c3c50ainfix &lt;=c0c50Iainfix =V1ainfix +V0c1FF">
shape="iainfix &lt;=c0c50ainfix &lt;=ainfix +V1c3c50ainfix &gt;=V1c42Iainfix =V1ainfix +V0c1FF">
<label
name="expl:VC for g"/>
<proof
......@@ -169,7 +169,7 @@
sum="0bd9218916f427e974654d2df2635b1c"
proved="true"
expanded="true"
shape="ainfix &lt;V0c1Aainfix &lt;c0V0NF">
shape="Nainfix &lt;V0c1Aainfix &lt;c0V0F">
<proof
prover="0"
timelimit="3"
......@@ -186,7 +186,7 @@
sum="d3230f57702882c340d643fad1ef16f5"
proved="false"
expanded="true"
shape="ainfix &lt;=V0c1Aainfix &lt;=c0V0NF">
shape="Nainfix &lt;=V0c1Aainfix &lt;=c0V0F">
<proof
prover="0"
timelimit="3"
......@@ -363,7 +363,7 @@
sum="ca65487ca829d6a30999c0820737fbce"
proved="false"
expanded="true"
shape="ainfix &lt;V0c1.0Aainfix &lt;c0.0V0NF">
shape="Nainfix &lt;V0c1.0Aainfix &lt;c0.0V0F">
<proof
prover="0"
timelimit="3"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......@@ -617,7 +617,7 @@
sum="f7653853a52697d18d92afe29d168745"
proved="true"
expanded="false"
shape="ainfix =aceilainfix /.V0V1c0NIainfix &gt;V1c0.0Aainfix &gt;V0c0.0F">
shape="Nainfix =aceilainfix /.V0V1c0Iainfix &gt;V1c0.0Aainfix &gt;V0c0.0F">
<proof
prover="0"
timelimit="5"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Coq"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Alt-Ergo"
......@@ -529,7 +529,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.65"/>
<result status="timeout" time="4.96"/>
</proof>
<proof
prover="10"
......@@ -626,7 +626,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.66"/>
<result status="timeout" time="4.98"/>
</proof>
<proof
prover="10"
......@@ -723,7 +723,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.65"/>
<result status="timeout" time="4.96"/>
</proof>
<proof
prover="10"
......@@ -820,7 +820,7 @@
memlimit="4000"
obsolete="false"
archived="false">
<result status="timeout" time="5.64"/>
<result status="timeout" time="4.97"/>
</proof>
<proof
prover="10"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<why3session shape_version="3">
<prover
id="0"
name="Gappa"
......
This diff is collapsed.
......@@ -60,7 +60,7 @@ let debug = Debug.register_info_flag "session_pairing"
~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \
session@ trees@ after@ modification@ of@ source@ files."
let current_shape_version = 2
let current_shape_version = 3
(* similarity code of terms, or of "shapes"
......@@ -135,17 +135,35 @@ let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a =
List.fold_left fn
(ident_shape ~push s.ls_name (push tag_app acc))
l
| Tif (f,t1,t2) -> fn (fn (fn (push tag_if acc) t2) t1) f
| Tif (f,t1,t2) ->
begin match version with
| 1 | 2 -> fn (fn (fn (push tag_if acc) f) t1) t2
| 3 -> fn (fn (fn (push tag_if acc) t2) t1) f
| _ -> assert false
end
| Tcase (t1,bl) ->
let br_shape acc b =
let p,t2 = t_open_branch b in
let m1 = pat_rename_alpha c m p in
let acc = t_shape ~version ~push c m1 acc t2 in
pat_shape ~push c m acc p
match version with
| 1 | 2 ->
let acc = pat_shape ~push c m acc p in
let m = pat_rename_alpha c m p in
t_shape ~version ~push c m acc t2
| 3 ->
let m1 = pat_rename_alpha c m p in
let acc = t_shape ~version ~push c m1 acc t2 in
pat_shape ~push c m acc p
| _ -> assert false
in
let acc = push tag_case acc in
let acc = List.fold_left br_shape acc bl in
fn acc t1
begin match version with
| 1 | 2 ->
List.fold_left br_shape (fn (push tag_case acc) t1) bl
| 3 ->
let acc = push tag_case acc in
let acc = List.fold_left br_shape acc bl in
fn acc t1
| _ -> assert false
end
| Teps b ->
let u,f = t_open_bound b in
let m = vs_rename_alpha c m u in
......@@ -180,12 +198,17 @@ let rec t_shape ~version ~(push:string->'a->'a) c m (acc:'a) t : 'a =
match version with
| 1 ->
t_shape ~version ~push c m (fn (push tag_let acc) t1) t2
| 2 ->
| 2 | 3 ->
(* t2 first, intentionally *)
fn (push tag_let (t_shape ~version ~push c m acc t2)) t1
| _ -> assert false
end
| Tnot f -> fn (push tag_not acc) f
| Tnot f ->
begin match version with
| 1 | 2 -> push tag_not (fn acc f)
| 3 -> fn (push tag_not acc) f
| _ -> assert false
end
| Ttrue -> push tag_true acc
| Tfalse -> push tag_false acc
......@@ -198,8 +221,13 @@ let t_shape_buf ?(version=current_shape_version) t =
let t_shape_task ?(version=current_shape_version) t =
let b = Buffer.create 17 in
let push t () = Buffer.add_string b t in
let _, expl, _ = goal_expl_task ~root:false t in
Opt.iter (Buffer.add_string b) expl;
begin match version with
| 1 | 2 -> ()
| 3 ->
let _, expl, _ = goal_expl_task ~root:false t in
Opt.iter (Buffer.add_string b) expl
| _ -> assert false
end;
let f = Task.task_goal_fmla t in
let () = t_shape ~version ~push (ref (-1)) Mvs.empty () f in
Buffer.contents b
......
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