From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 28 May 2018 15:08:46 +0000 (+0200)
Subject: Tentative implementation of strong separation algorithm
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a57b32e5e068d05c1feb7455861bc8d5e4bd05a;p=fireball-separation.git

Tentative implementation of strong separation algorithm

- A `Match from num is translated to pure by masking branches
  with underscore lambdas
- The eating step on the divergent does not create a substitution in sigma
  (to be understood...)
- In the branch of matches, \_. !divergent is translated to delta
- The checks in dangerous must still be fixed to go under lambdas
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index c6cecec..311537a 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -3,7 +3,7 @@ open Util.Vars
 open Pure
 open Num
 
-let bomb = ref(`Var(-1,-666));;
+let divergent = ref(`Var(-1, -666));;
 
 (*
  The number of arguments which can applied to numbers
@@ -436,21 +436,8 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
   | Some div ->
    if List.mem (hd_of_i_var div) inedible
    then p
-   else
-    let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
-    let p, bomb' = make_fresh_var p (-666) in
-    (if !bomb <> `Var (-1,-666) then
-     failwithProblem p
-      ("Bomb was duplicated! It was " ^ string_of_nf !bomb ^
-       ", tried to change it to " ^ string_of_nf bomb'));
-    bomb := bomb';
-    prerr_endline ("Just created bomb var: " ^ string_of_nf !bomb);
-    let x = hd_of_i_var div in
-    let inst = make_lams !bomb n in
-    let p = {p with div=None} in
-    (* subst_in_problem (hd_of_i_var div) inst p in *)
-     {p with sigma=p.sigma@[x,inst]} in
-     let dangerous_conv = showstoppers_conv in
+   else (divergent := `Var(hd_of_i_var div, -666); {p with div=None}) in
+ let dangerous_conv = showstoppers_conv in
 prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
 List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
  let conv =
@@ -486,8 +473,6 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.
   `Continue p
 
 let instantiate p x n =
- (if hd_of_i_var (cast_to_i_var !bomb) = x
-   then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!"));
  let arity_of_x = max_arity_tms x (all_terms p) in
  (if arity_of_x = None then failwithProblem p "step on var non occurring in problem");
  (if Util.option_get(arity_of_x) = min_int then failwithProblem p "step on fake variable");
@@ -656,10 +641,7 @@ let env_of_sigma freshno sigma should_explode =
    (try
     e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
    with
-    Not_found ->
-    if n = hd_of_i_var (cast_to_i_var !bomb)
-     then ([], Pure.omega should_explode, [])
-     else ([], Pure.V n, []) ) :: e
+    Not_found -> ([], Pure.V n, []) ) :: e
  in aux 0
 ;;
 (* ************************************************************************** *)
@@ -692,7 +674,6 @@ let solve p =
  match check p with
  | Some s -> `Unseparable s
  | None ->
- bomb := `Var(-1,-666);
  Console.print_hline();
  let p_finale = auto p p.initialSpecialK in
  let freshno,sigma = p_finale.freshno, p_finale.sigma in
@@ -706,6 +687,7 @@ let solve p =
   (string_of_var p_finale.var_names x ^ " := " ^ string_of_term p_finale inst)) sigma;
 
  prerr_endline "---------<PURE>---------";
+ ToScott.bomb := !divergent;
  let scott_of_nf t = ToScott.t_of_nf (t :> nf) in
  let div = option_map scott_of_nf p.div in
  let conv = List.map scott_of_nf p.conv in
diff --git a/ocaml/num.ml b/ocaml/num.ml
index e7b6290..8ecf124 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -92,14 +92,23 @@ let free_vars = (List.map fst) ++ free_vars';;
 module ToScott =
 struct
 
+let delta = let open Pure in L(A(V 0, V 0))
+
+let bomb = ref(`Var(-1, -666));;
+
 let rec t_of_i_num_var =
  function
   | `N n -> Scott.mk_n n
-  | `Var(v,_) -> Pure.V v
+  | `Var(v,_) as x -> assert (x <> !bomb); Pure.V v
   | `Match(t,_,liftno,bs,args) ->
-      let bs = List.map (fun (n,t) -> n, t_of_nf (lift liftno t)) !bs in
+      let bs = List.map (
+        function (n,t) -> n,
+         (if t = !bomb then delta
+          else L (t_of_nf (lift (liftno+1) t)))
+        ) !bs in
       let t = t_of_i_num_var t in
       let m = Scott.mk_match t bs in
+      let m = Pure.A(m,delta) in
       List.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) m args
   | `I((v,_), args) -> Listx.fold_left (fun acc t -> Pure.A(acc,t_of_nf t)) (Pure.V v) args
 and t_of_nf =
diff --git a/ocaml/num.mli b/ocaml/num.mli
index c7b3256..f1ea4f8 100644
--- a/ocaml/num.mli
+++ b/ocaml/num.mli
@@ -26,6 +26,7 @@ val free_vars' : nf -> var list
 val free_vars : nf -> int list
 module ToScott :
   sig
+    val bomb : nf ref
     val t_of_i_num_var : nf i_num_var_ -> Pure.Pure.t
     val t_of_nf : nf -> Pure.Pure.t
   end
diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index f1cac84..7963f87 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -94,6 +94,7 @@ in
    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, []
      | (e,A(t1,t2),s) ->
          let t2' = aux g (e,t2,[]) in
          let (_,t,_) = t2' in