Skip to content

Commit 3cd1fa0

Browse files
lyonel2017lyonel2017
committed
Some fixes
1 parent 2719b38 commit 3cd1fa0

File tree

16 files changed

+93
-82
lines changed

16 files changed

+93
-82
lines changed

‎examples/exception.ec‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,15 +21,15 @@ hoare [M'.truc : _x = x ==> false | assume:p1 _x | assert: !(p1 _x /\ p2 _x)].
2121
proof.
2222
proc.
2323
wp.
24-
auto => &hr <- />. smt.
24+
auto => &hr <- /> /#.
2525
qed.
2626

2727
lemma assert_assume (_x:int):
2828
hoare [M'.truc : _x = x ==> false | assume:p2 _x | assert: !(p2 _x /\ p1 _x) ].
2929
proof.
3030
proc.
3131
wp.
32-
auto => &hr <- />. smt.
32+
auto => &hr <- /> /#.
3333
qed.
3434

3535
lemma assert_assume' ( _x:int) :
@@ -82,7 +82,7 @@ hoare [M.f1 : _x = x ==> (res <= 5) | e1:_x <= 3 | pd1].
8282
proof.
8383
proc.
8484
conseq (: _ ==> x = 5 | e1: _x = 3 | e2: pe | pd2).
85-
+ move => &hr h x. smt.
85+
+ move => &hr h x. smt(a1 a2).
8686
+ wp. auto.
8787
qed.
8888

@@ -94,9 +94,9 @@ hoare [M.f2 : _x = x ==> res < 6 | e1: _x < 4 | e2:pe3 | e3: pe4 | pd2 ].
9494
+ call (: _x = x ==> res = 5 | e1 : 3 = _x | e2: pd2 | pd2).
9595
+ proc.
9696
wp. auto.
97-
wp. auto. smt.
97+
wp. auto. smt(a4 a3).
9898
call (l_f1 _x).
99-
auto. smt.
99+
auto. smt(a5 a3 a4).
100100
qed.
101101

102102
module M1 ={

‎src/ecAst.ml‎

Lines changed: 35 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -496,11 +496,10 @@ let lift_ss_inv2 (f: ss_inv -> ss_inv -> 'a) : inv -> inv -> 'a =
496496

497497
let lift_hs_ss_inv (f: ss_inv -> hs_inv -> 'a) : inv -> inv -> 'a =
498498
let f inv1 inv2 = match inv1, inv2 with
499-
| Inv_ss ss1, Inv_hs ss2 -> f ss1 ss2
500-
| _ -> failwith "expected only single sided invariants" in
499+
| Inv_ss ss_inv, Inv_hs hs_inv -> f ss_inv hs_inv
500+
| _ -> failwith "expected single sided invariants and hoare invariant" in
501501
f
502502

503-
504503
let lift_ss_inv3 (f: ss_inv -> ss_inv -> ss_inv -> 'a) : inv -> inv -> inv -> 'a =
505504
let f inv1 inv2 inv3 = match inv1, inv2, inv3 with
506505
| Inv_ss ss1, Inv_ss ss2, Inv_ss ss3 -> f ss1 ss2 ss3
@@ -537,15 +536,15 @@ let map_inv (fn: form list -> form) (inv: inv list): inv =
537536
Inv_ts (map_ts_inv fn (List.map (function
538537
Inv_ts ts -> assert (ts.ml = ts'.ml && ts.mr = ts'.mr); ts
539538
| _ -> failwith "expected all invariants to have same kind") inv))
540-
| _ -> failwith "Patch Inv_hs"
539+
| _ -> failwith "Exceptions are not supported"
541540

542541
let map_inv1 (fn: form -> form) (inv: inv): inv =
543542
match inv with
544543
| Inv_ss ss ->
545544
Inv_ss (map_ss_inv1 fn ss)
546545
| Inv_ts ts ->
547-
Inv_ts (map_ts_inv1 fn ts)
548-
| _ -> failwith "Patch Inv_hs2"
546+
Inv_ts (map_ts_inv1 fn ts)
547+
| _ -> failwith "Exceptions are not supported"
549548

550549
let map_inv2 (fn: form -> form -> form) (inv1: inv) (inv2: inv): inv =
551550
match inv1, inv2 with
@@ -604,9 +603,9 @@ let map2_poe f (p1,m1,d1) (p2,m2,d2) =
604603
| _ , _ -> failwith "missing entry in exception map"
605604
in
606605
let m = DMap.merge aux m1 m2 in
607-
match d2, d1 with
606+
match d1, d2 with
608607
| None, None -> (p, m, None)
609-
| Some d2, Some d1 -> (p, m, Some (f d2 d1))
608+
| Some d1, Some d2 -> (p, m, Some (f d1 d2))
610609
| _, _ -> failwith "missing default exception"
611610

612611
let map_hs_inv2
@@ -642,12 +641,38 @@ let iter_poe f (p, m,d) =
642641

643642
let iter2_poe f (p1,m1,d1) (p2,m2,d2) =
644643
f p1 p2;
645-
DMap.iter (fun e1 p1 -> f (DMap.find e1 m2) p1) m1;
644+
let aux _ a b =
645+
match a, b with
646+
| Some a, Some b -> Some (a,b)
647+
| _ , _ -> failwith "missing entry in exception map"
648+
in
649+
let m = DMap.merge aux m1 m2 in
650+
DMap.iter (fun _ (p1,p2) -> f p1 p2) m;
646651
match d2, d1 with
647652
| None, None -> ()
648-
| Some d2, Some d1 -> f d2 d1
653+
| Some d1, Some d2 -> f d1 d2
649654
| _, _ -> failwith "missing default exception"
650655

656+
let merge2_poe_list f (poe1,d1) (poe2,d2) =
657+
let get_default d =
658+
match d with
659+
| Some d -> d
660+
| None -> failwith "no default exception"
661+
in
662+
let aux _ a b =
663+
match a,b with
664+
| Some a, Some b -> Some (f b a)
665+
| Some a, None -> Some (f (get_default d2) a)
666+
| None, Some b -> Some (f b (get_default d1))
667+
| None, None -> assert false
668+
in
669+
let epost = DMap.merge aux poe1 poe2 in
670+
let poe = List.map snd ( DMap.bindings epost) in
671+
match d2, d1 with
672+
| None, _ -> poe
673+
| Some d2, Some d1 -> f d2 d1 :: poe
674+
| _, _ -> failwith "no default exception"
675+
651676
(* ----------------------------------------------------------------- *)
652677
(* Accessors for program logic *)
653678
(* ----------------------------------------------------------------- *)

‎src/ecAst.mli‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -378,13 +378,21 @@ val lower_f : hs_inv -> ss_inv
378378
val update_hs_ss : ss_inv -> hs_inv -> hs_inv
379379
val map_poe : (form -> form) -> post -> post
380380
val map_hs_inv1 : (form -> form) -> hs_inv -> hs_inv
381+
val map2_poe :
382+
(form -> form -> 'a) -> post -> post -> 'a * (EcPath.path, 'a) DMap.t * 'a option
381383
val map_hs_inv2 : (form -> form -> form) -> hs_inv -> hs_inv -> hs_inv
382384
val exists_poe : (form -> bool) -> post -> bool
383385
val forall_poe : (form -> bool) -> post -> bool
384386
val forall2_poe : (form -> form -> bool) -> post -> post -> bool
385-
val poe_to_list : post -> form list
387+
val poe_to_list : 'a * (EcPath.path, 'a) DMap.t * 'a option -> 'a list
386388
val iter_poe : (form -> unit) -> post -> unit
387389
val iter2_poe : (form -> form -> unit) -> post -> post -> unit
390+
val merge2_poe_list :
391+
(form -> form -> form) ->
392+
(EcPath.path, form) DMap.t * form option ->
393+
(EcPath.path, form) DMap.t * form option ->
394+
form list
395+
388396

389397
(* -------------------------------------------------------------------- *)
390398

‎src/ecCorePrinting.ml‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -83,17 +83,17 @@ module type PrinterAPI = sig
8383
val pp_vsubst : PPEnv.t -> vsubst pp
8484

8585
(* ------------------------------------------------------------------ *)
86-
val pp_typedecl : PPEnv.t -> (path * tydecl ) pp
87-
val pp_opdecl : ?long:bool -> PPEnv.t -> (path * operator ) pp
88-
val pp_added_op : PPEnv.t -> operator pp
89-
val pp_axiom : ?long:bool -> PPEnv.t -> (path * axiom ) pp
90-
val pp_theory : PPEnv.t -> (path * ctheory ) pp
91-
val pp_modtype1 : PPEnv.t -> (module_type ) pp
92-
val pp_modtype : PPEnv.t -> (module_type ) pp
93-
val pp_modexp : PPEnv.t -> (mpath * module_expr ) pp
94-
val pp_moditem : PPEnv.t -> (mpath * module_item ) pp
95-
val pp_modsig : ?long:bool -> PPEnv.t -> (path * module_sig) pp
96-
val pp_modsig_smpl : PPEnv.t -> (path * module_smpl_sig ) pp
86+
val pp_typedecl : PPEnv.t -> (path * tydecl ) pp
87+
val pp_opdecl : ?long:bool -> PPEnv.t -> (path * operator ) pp
88+
val pp_added_op : PPEnv.t -> operator pp
89+
val pp_axiom : ?long:bool -> PPEnv.t -> (path * axiom ) pp
90+
val pp_theory : PPEnv.t -> (path * ctheory ) pp
91+
val pp_modtype1 : PPEnv.t -> (module_type ) pp
92+
val pp_modtype : PPEnv.t -> (module_type ) pp
93+
val pp_modexp : PPEnv.t -> (mpath * module_expr ) pp
94+
val pp_moditem : PPEnv.t -> (mpath * module_item ) pp
95+
val pp_modsig : ?long:bool -> PPEnv.t -> (path * module_sig) pp
96+
val pp_modsig_smpl : PPEnv.t -> (path * module_smpl_sig ) pp
9797

9898
(* ------------------------------------------------------------------ *)
9999
val pp_hoareS : PPEnv.t -> ?prpo:prpo_display -> sHoareS pp

‎src/ecMaps.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -186,6 +186,6 @@ end = struct
186186
f prefix t.value;
187187
Map.iter (fun k v -> doit (k :: prefix) v) t.children
188188
in
189-
189+
190190
doit [] t
191191
end

‎src/ecMatching.ml‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -695,8 +695,16 @@ let f_match_core opts hyps (ue, ev) f1 f2 =
695695
Fsubst.f_bind_mem subst hf1.hf_m hf2.hf_m in
696696
assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs));
697697
let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in
698-
let lf1 = poe_to_list (hf_po hf1).hsi_inv in
699-
let lf2 = poe_to_list (hf_po hf2).hsi_inv in
698+
let poe2 =
699+
EcAst.map2_poe
700+
(fun a b -> (a,b))
701+
(hf_po hf1).hsi_inv
702+
(hf_po hf2).hsi_inv
703+
in
704+
let lpoe2 = poe_to_list poe2 in
705+
let lf1 = List.map fst lpoe2 in
706+
let lf2 = List.map snd lpoe2 in
707+
700708
List.iter2 (doit env (subst, mxs))
701709
((hf_pr hf1).inv :: lf1) ((hf_pr hf2).inv :: lf2)
702710
end

‎src/ecPath.ml‎

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ and path_node =
1717
(* -------------------------------------------------------------------- *)
1818
let p_equal = ((==) : path -> path -> bool)
1919
let p_hash = fun p -> p.p_tag
20-
let p_node = fun p -> p.p_node
2120
let p_compare = fun p1 p2 -> p_hash p1 - p_hash p2
2221

2322
module Hspath = Why3.Hashcons.Make (struct
@@ -60,14 +59,6 @@ let rec p_ntr_compare (p1 : path) (p2 : path) =
6059
| n -> n
6160
end
6261

63-
let rec p_ntr_equal (p1 : path) (p2 : path) =
64-
match p1.p_node, p2.p_node with
65-
| Psymbol x1, Psymbol x2 ->
66-
String.equal x1 x2
67-
| Pqname (p1, x1), Pqname (p2, x2) ->
68-
p_ntr_equal p1 p2 && String.equal x1 x2
69-
| _, _ -> false
70-
7162
(* -------------------------------------------------------------------- *)
7263
module Mp = Path.M
7364
module Hp = Path.H

‎src/ecPath.mli‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ val poappend : path -> path option -> path
2222

2323
val p_equal : path -> path -> bool
2424
val p_compare : path -> path -> int
25-
val p_ntr_equal : path -> path -> bool
2625
val p_ntr_compare : path -> path -> int
2726
val p_hash : path -> int
2827

‎src/ecProofTyping.ml‎

Lines changed: 0 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -268,24 +268,3 @@ let destruct_exists ?(reduce = true) hyps fp : dexists option =
268268
| _ -> raise NoMatch
269269
in
270270
lazy_destruct ~reduce hyps doit fp
271-
272-
(* -------------------------------------------------------------------- *)
273-
let merge2_poe_list f (poe1,d1) (poe2,d2) =
274-
let get_default d =
275-
match d with
276-
| Some d -> d
277-
| None -> failwith "no default exception"
278-
in
279-
let aux _ a b =
280-
match a,b with
281-
| Some a, Some b -> Some (f b a)
282-
| Some a, None -> Some (f (get_default d2) a)
283-
| None, Some b -> Some (f b (get_default d1))
284-
| None, None -> assert false
285-
in
286-
let epost = DMap.merge aux poe1 poe2 in
287-
let poe = List.map snd ( DMap.bindings epost) in
288-
match d2, d1 with
289-
| None, _ -> poe
290-
| Some d2, Some d1 -> f d2 d1 :: poe
291-
| _, _ -> failwith "no default exception"

‎src/ecProofTyping.mli‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -81,11 +81,3 @@ type dexists = [
8181

8282
val destruct_product: ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dproduct option
8383
val destruct_exists : ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dexists option
84-
85-
(* -------------------------------------------------------------------- *)
86-
87-
val merge2_poe_list :
88-
(form -> form -> form) ->
89-
(EcPath.path, form) DMap.t * form option ->
90-
(EcPath.path, form) DMap.t * form option ->
91-
form list

0 commit comments

Comments
 (0)