transformation compute: check vars of lefthand sides

src/transform/compute.ml

@@ -26,7 +26,7 @@ let meta_compute_max_steps = Theory.register_meta_excl "compute_max_steps"
   ~desc:"Maximal@ number@ of@ reduction@ steps@ done@ by@ compute@ \
          transformation"
 
-let compute_max_steps = ref 1000
+let compute_max_steps = ref 1024
 
 (* not yet used
 let meta_begin_compute_context =

src/transform/reduction_engine.ml

@@ -987,8 +987,19 @@ let extract_rule _km t =
       | Decl.Dparam _ | Decl.Dind _ -> ()
   in
 *)
-  (* TODO : verifier que les variables de droite, aussi bien term que type,
-     apparaissent a gauche *)
+
+  let check_vars acc t1 t2 =
+    (* check that quantified variables all appear in the lefthand side *)
+    let vars_lhs = t_vars t1 in
+    if Svs.exists (fun vs -> not (Mvs.mem vs vars_lhs)) acc
+    then raise (NotARewriteRule "lhs should contain all variables");
+    (* check the same with type variables *)
+    if not
+         (Ty.Stv.subset
+            (t_ty_freevars Ty.Stv.empty t2) (t_ty_freevars Ty.Stv.empty t2))
+    then raise (NotARewriteRule "lhs should contain all type variables")
+
+  in
 
   let rec aux acc t =
     match t.t_node with
@@ -998,14 +1009,20 @@ let extract_rule _km t =
       | Tbinop(Tiff,t1,t2) ->
         begin
           match t1.t_node with
-            | Tapp(ls,args) -> (* check_ls ls; *) acc,ls,args,t2
+            | Tapp(ls,args) ->
+               (* check_ls ls; *)
+               check_vars acc t1 t2;
+               acc,ls,args,t2
             | _ -> raise
               (NotARewriteRule "lhs of <-> should be a predicate symbol")
         end
       | Tapp(ls,[t1;t2]) when ls == ps_equ ->
         begin
           match t1.t_node with
-            | Tapp(ls,args) -> (* check_ls ls; *) acc,ls,args,t2
+            | Tapp(ls,args) ->
+               (* check_ls ls; *)
+               check_vars acc t1 t2;
+               acc,ls,args,t2
             | _ -> raise
               (NotARewriteRule "lhs of = should be a function symbol")
         end

tests/test_compute.why

@@ -10,7 +10,7 @@ constant a : int
 
 goal g1: f 42 = a
 
-constant compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) = 
+constant compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c) =
          (\f:'b->'c.(\g:'a->'b.(\x:'a.f (g x))))
 
 goal g2: compose f f 42 = a
@@ -39,7 +39,7 @@ theory A
   type t
 
   function f t : bool
-  predicate r t 
+  predicate r t
 
   axiom a : forall x:t. f x = True <-> r x
 
@@ -119,7 +119,7 @@ theory TestArith
 
 
   function f int : int
-  
+
   axiom a42 : f 42 + 43 = 56
 
   meta rewrite prop a42
@@ -353,7 +353,7 @@ theory Rinteger
    function f int : int
 
    goal g3 : (f 1 + f 2) + f 3 = f 4
- 
+
 end
 
 theory TestInteger
@@ -406,3 +406,19 @@ goal g02 : mem A (union (add B empty) (add C empty))
 goal g025 : mem A (union (singleton B) (singleton C))
 
 end
+
+
+theory Wrong
+
+type t
+
+constant a : t
+constant b : t
+
+axiom A : forall x:t. a = x
+
+meta "rewrite" prop A
+
+goal test : a = b
+
+end
\ No newline at end of file

tests/test_compute/why3session.xml

@@ -3,7 +3,7 @@
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
 <file name="../test_compute.why" expanded="true">
-<theory name="Lambda" sum="ac7b1c25f8dd32d440e0b14d115c7c15" expanded="true">
+<theory name="Lambda" sum="eccefff73b61d59406c27a0c2728956d" expanded="true">
  <goal name="g1" expanded="true">
  <transf name="compute_in_goal" expanded="true">
   <goal name="g1.1" expl="1.">
@@ -23,20 +23,20 @@
  </transf>
  </goal>
 </theory>
-<theory name="A" sum="0e4355327797e8f3d23d6df80a329362" expanded="true">
+<theory name="A" sum="d9ba1fe2e9cce711ff1365afa1a34c8a" expanded="true">
  <goal name="G1">
  </goal>
  <goal name="G2">
  </goal>
  <goal name="G3">
  </goal>
- <goal name="g" expanded="true">
+ <goal name="g">
  <transf name="compute_in_goal">
  </transf>
  </goal>
 </theory>
-<theory name="Test" sum="cd473d7e70fa0fdfbc7f9f5523952c9e" expanded="true">
- <goal name="g1" expanded="true">
+<theory name="Test" sum="dc2b4bcf8c22d5571bbed8cb811c4ee5" expanded="true">
+ <goal name="g1">
  <transf name="compute_in_goal">
  </transf>
  </goal>
@@ -46,43 +46,43 @@
   </goal>
  </transf>
  </goal>
- <goal name="g3" expanded="true">
+ <goal name="g3">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="g10" expanded="true">
+ <goal name="g10">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="g11" expanded="true">
+ <goal name="g11">
  <transf name="compute_in_goal">
  </transf>
  </goal>
 </theory>
-<theory name="TestArith" sum="cf84efb4f92d0a90148d60fc86520337" expanded="true">
- <goal name="h1" expanded="true">
+<theory name="TestArith" sum="1d7cdddf59d040c2052a710a100476da" expanded="true">
+ <goal name="h1">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="h2" expanded="true">
+ <goal name="h2">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="h3" expanded="true">
+ <goal name="h3">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="j1" expanded="true">
+ <goal name="j1">
  <transf name="compute_in_goal">
  </transf>
  </goal>
  <goal name="k1">
  </goal>
- <goal name="l1" expanded="true">
+ <goal name="l1">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="l2" expanded="true">
+ <goal name="l2">
  <transf name="compute_in_goal">
  </transf>
  </goal>
@@ -100,15 +100,15 @@
   </goal>
  </transf>
  </goal>
- <goal name="l6" expanded="true">
+ <goal name="l6">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="l7" expanded="true">
+ <goal name="l7">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="l8" expanded="true">
+ <goal name="l8">
  <transf name="compute_in_goal">
  </transf>
  </goal>
@@ -165,26 +165,26 @@
  </transf>
  </goal>
 </theory>
-<theory name="TestRecord" sum="01e5c2659bedbfaf6934498a0580aaef" expanded="true">
- <goal name="i1" expanded="true">
+<theory name="TestRecord" sum="50e2f31a6393b25939c90eda521bdb36">
+ <goal name="i1">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="i2" expanded="true">
+ <goal name="i2">
  <transf name="compute_in_goal">
  </transf>
  </goal>
 </theory>
-<theory name="TestList" sum="ec36d89b8213f71e7ce492154030a520" expanded="true">
- <goal name="g1" expanded="true">
+<theory name="TestList" sum="dd44c95c50aa3d0f50260c2b24d84ac5" expanded="true">
+ <goal name="g1">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="g2" expanded="true">
+ <goal name="g2">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="g3" expanded="true">
+ <goal name="g3">
  <transf name="compute_in_goal">
  </transf>
  </goal>
@@ -194,7 +194,7 @@
   </goal>
  </transf>
  </goal>
- <goal name="h2" expanded="true">
+ <goal name="h2">
  <transf name="compute_in_goal">
  </transf>
  </goal>
@@ -211,9 +211,9 @@
  </transf>
  </goal>
 </theory>
-<theory name="Rstandard" sum="d15a33b5087e18703e665562df77da7b" expanded="true">
+<theory name="Rstandard" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="TestStandard" sum="2fd3eb677ecb57f8070b869da5d28004" expanded="true">
+<theory name="TestStandard" sum="e6f40d1a540fe93361cf8f2931535b04" expanded="true">
  <goal name="g00" expanded="true">
  <transf name="compute_in_goal" expanded="true">
   <goal name="g00.1" expl="1.">
@@ -259,14 +259,14 @@
  </transf>
  </goal>
 </theory>
-<theory name="Rgroup" sum="8030b6755c9fc45b022c7e02bda40fe0" expanded="true">
+<theory name="Rgroup" sum="4638d2bcbe6996b18cb366b765d6773c" expanded="true">
  <goal name="g0" expanded="true">
  <transf name="compute_in_goal" expanded="true">
   <goal name="g0.1" expl="1.">
   </goal>
  </transf>
  </goal>
- <goal name="g01" expanded="true">
+ <goal name="g01">
  <transf name="compute_in_goal">
  </transf>
  </goal>
@@ -276,12 +276,12 @@
   </goal>
  </transf>
  </goal>
- <goal name="g2" expanded="true">
+ <goal name="g2">
  <transf name="compute_in_goal">
  </transf>
  </goal>
 </theory>
-<theory name="NonTerm" sum="87ef3d7b5b86367abfb7970651e260bb" expanded="true">
+<theory name="NonTerm" sum="3aebbc4daaeb7b2edf405b33e9357c69" expanded="true">
  <goal name="g" expanded="true">
  </goal>
  <goal name="g3" expanded="true">
@@ -337,9 +337,7 @@
  </transf>
  </goal>
 </theory>
-<theory name="Rinteger" sum="2f122a5715db5cd8f4e556ad50e7e93a" expanded="true">
- <goal name="l1" expanded="true">
- </goal>
+<theory name="Rinteger" sum="43b99dccfd03d9d03e3c394a20de09d8" expanded="true">
  <goal name="g1" expanded="true">
  <transf name="compute_in_goal" expanded="true">
   <goal name="g1.1" expl="1.">
@@ -348,26 +346,30 @@
  </goal>
  <goal name="g2" expanded="true">
  </goal>
+ <goal name="l1" expanded="true">
+ </goal>
+ <goal name="g3" expanded="true">
+ </goal>
 </theory>
-<theory name="TestInteger" sum="78e4952fbe0b5a41d4090c065e7fb7da" expanded="true">
+<theory name="TestInteger" sum="8213e2f3d6fba0e4061fbf086fa95cd4" expanded="true">
  <goal name="g1" expanded="true">
  <transf name="compute_in_goal" expanded="true">
   <goal name="g1.1" expl="1.">
   </goal>
  </transf>
  </goal>
- <goal name="g2" expanded="true">
+ <goal name="g2">
  <transf name="compute_in_goal">
  </transf>
  </goal>
- <goal name="g3" expanded="true">
+ <goal name="g3">
  <transf name="compute_in_goal">
  </transf>
  </goal>
 </theory>
-<theory name="MoreSets" sum="01291474093c6b040239f432b3e29a68" expanded="true">
+<theory name="MoreSets" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
 </theory>
-<theory name="TestSets" sum="58259bcc10097e7916eb0df798bda319" expanded="true">
+<theory name="TestSets" sum="b19615af2af0ed66bcf0212fb6d0b56f" expanded="true">
  <goal name="g00" expanded="true">
  <transf name="compute_in_goal" expanded="true">
   <goal name="g00.1" expl="1.">
@@ -399,5 +401,9 @@
  </transf>
  </goal>
 </theory>
+<theory name="Wrong" sum="1820619dc61b06ee59d47a1e7b068c87" expanded="true">
+ <goal name="test" expanded="true">
+ </goal>
+</theory>
 </file>
 </why3session>