From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 16:27:51 +0000 (+0200)
Subject: New (in-)decision procedure for termination
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e5e1945c99404f171f90a93c18c336aaeaab546;p=fireball-separation.git

New (in-)decision procedure for termination
---

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 11cb9af..3bd7ec4 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -90,11 +90,20 @@ in
      String.concat "," (List.map print_machine s) ^ "]"
 ;; *)
 
+  let omega = let delta = L(A(V 0, V 0)) in A(delta,delta)
+
+  let rec is_divergent =
+   function
+      t when t = omega -> true
+    | A(t,_) -> is_divergent t
+    | L(t) -> is_divergent t
+    | _ -> false
+
   let mwhd m =
    let rec aux g =
     function
     (* mmm -> print_endline (print_machine mmm); match mmm with *)
-        m when unwind m = let d = L(A(V 0, V 0)) in A(d,d) -> [], B, []
+        m when is_divergent (unwind m) -> [], B, []
      | (e,A(t1,t2),s) ->
          let t2' = aux g (e,t2,[]) in
          let (_,t,_) = t2' in