SOUNDNESS : the e.v.c. must ensure distinctness of e.v.s

chaudhuri · Feb 26, 2015 · d4a8532 · d4a8532
1 parent 3d8733a
commit d4a8532
Show file tree

Hide file tree

Showing 2 changed files with 66 additions and 26 deletions.
diff --git a/src/inverse.ml b/src/inverse.ml
@@ -65,6 +65,28 @@ let rec spin_until_quiescence measure op =
   let after = measure () in
   if before != after then spin_until_quiescence measure op
 
+let rec percolate ~sc_fact ~sc_rule rules iter =
+  let new_rules = percolate_once ~sc_fact rules iter in
+  List.iter sc_rule new_rules ;
+  if new_rules <> [] then percolate ~sc_fact ~sc_rule new_rules iter
+
+and percolate_once ~sc_fact rules iter =
+  let new_rules = ref [] in
+  let add_rule rr =
+    match rr.prems with
+    | [] -> sc_fact rr.concl
+    | _ -> new_rules := rr :: !new_rules
+  in
+  List.iter begin fun rr ->
+    iter begin fun sq ->
+      Rule.specialize_default rr sq
+        ~sc_fact
+        ~sc_rule:add_rule
+    end
+  end rules ;
+  !new_rules
+
+
 let noop () = ()
 
 module Inv (D : Data) = struct
@@ -95,29 +117,33 @@ module Inv (D : Data) = struct
       gen ~sc:add_rule ;
       spin_until_none D.select begin fun sel ->
         (* Format.printf "Selected: %a@." (Sequent.format_sequent ()) sel ; *)
-        let new_rules = ref [] in
-        let add_new_rule rr =
-          match rr.prems with
-          | [] ->  add_seq rr.concl
-          | _ ->
-              (* Rule.Test.print rr ; *)
-              new_rules := rr :: !new_rules
-        in
-        List.iter begin fun rr ->
-          Rule.specialize_default rr sel
-            ~sc_rule:add_new_rule
-            ~sc_fact:add_seq ;
-        end !rules ;
-        spin_until_quiescence (fun () -> List.length !new_rules) begin fun () ->
-          List.iter begin fun rr ->
-            D.iter_active begin fun act ->
-              Rule.specialize_default rr act
-                ~sc_rule:add_new_rule
-                ~sc_fact:add_seq
-            end
-          end !new_rules ;
-        end ;
-        List.iter add_rule !new_rules ;
+        (* let new_rules = ref [] in *)
+        (* let add_new_rule rr = *)
+        (*   match rr.prems with *)
+        (*   | [] ->  add_seq rr.concl *)
+        (*   | _ -> *)
+        (*       Rule.Test.print rr ; *)
+        (*       new_rules := rr :: !new_rules *)
+        (* in *)
+        percolate !rules (fun doit -> doit sel)
+          ~sc_rule:add_rule ~sc_fact:add_seq ;
+        (* List.iter begin fun rr -> *)
+        (*   Rule.specialize_default rr sel *)
+        (*     ~sc_rule:add_new_rule *)
+        (*     ~sc_fact:add_seq ; *)
+        (* end !rules ; *)
+        percolate !rules D.iter_active
+          ~sc_rule:add_rule ~sc_fact:add_seq ;
+        (* spin_until_quiescence (fun () -> List.length !new_rules) begin fun () -> *)
+        (*   List.iter begin fun rr -> *)
+        (*     D.iter_active begin fun act -> *)
+        (*       Rule.specialize_default rr act *)
+        (*         ~sc_rule:add_new_rule *)
+        (*         ~sc_fact:add_seq *)
+        (*     end ; *)
+        (*   end !new_rules ; *)
+        (* end ; *)
+        (* List.iter add_rule !new_rules ; *)
         per_loop () ;
       end ;
       None

diff --git a/src/rule.ml b/src/rule.ml
@@ -106,7 +106,8 @@ let rule_match_exn ~sc prem cand =
         (repl, prem.right, false)
     | Some (p, pargs), Some (q, qargs) -> begin
         if p != q then Unify.unif_fail "right hand sides" ;
-        let (repl, args) = Unify.unite_match_lists repl pargs qargs in
+        (* let (repl, args) = Unify.unite_match_lists repl pargs qargs in *)
+        let (repl, args) = Unify.unite_lists repl pargs qargs in
         (repl, Some (p, args), true)
       end
   in
@@ -150,7 +151,8 @@ let rule_match_exn ~sc prem cand =
             (*     (format_term ()) (app q qargs) *)
             (*     format_repl repl ; *)
             (* ) ; *)
-            let (repl, _) = Unify.unite_match_lists repl pargs qargs in
+            (* let (repl, _) = Unify.unite_match_lists repl pargs qargs in *)
+            let (repl, _) = Unify.unite_lists repl pargs qargs in
             (* Format.( *)
             (*   eprintf "rule_match: hyp matched with %a@." format_repl repl *)
             (* ) ; *)
@@ -190,8 +192,20 @@ let specialize_one ~sc ~sq ~concl ~eigen current_prem remaining_prems =
       in
       let prems = List.map (distribute sq.right) prems in
       let concl = distribute sq.right concl in
+      let old_eigen = eigen in
       let eigen = replace_eigen_set ~repl eigen in
-      if not @@ ec_viol eigen concl then
+      (* if IdtSet.cardinal old_eigen <> IdtSet.cardinal eigen then *)
+      (*   Format.( *)
+      (*     eprintf "old_eigen: %s@." (IdtSet.elements old_eigen |> *)
+      (*                                List.map (fun x -> x.rep) |> *)
+      (*                                String.concat ",") ; *)
+      (*     eprintf "eigen: %s@." (IdtSet.elements eigen |> *)
+      (*                            List.map (fun x -> x.rep) |> *)
+      (*                            String.concat ",") ; *)
+      (*   ) ; *)
+      if IdtSet.cardinal old_eigen == IdtSet.cardinal eigen &&
+         not @@ ec_viol eigen concl
+      then
         let prem_vars = List.fold_left begin
             fun vars sq -> IdtSet.union vars sq.vars
           end IdtSet.empty prems in