From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 14 Jul 2017 17:39:21 +0000 (+0200)
Subject: Failure in case of empty problem, to be fixed
X-Git-Tag: weak-reduction-separation~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=61bc6d66eebfaa4649094b3ee8b2d5317d8f8346;p=fireball-separation.git

Failure in case of empty problem, to be fixed

(cherry picked from commit 605ae9159149e42a17f044bbfad94f7dc2de79c2)
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 4108ea5..a8899bc 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -757,14 +757,14 @@ let tmp (label, div, conv, nums, var_names) =
 
  (* TODO: *)
  (* replace div with bottom in problem??? *)
- let special_k =
-  let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
-  compute_special_k (Listx.from_list (all_tms :> nf list)) in (* compute initial special K *)
+ let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
+ if all_tms = [] then failwith "FIXME: empty problem";
+ let initialSpecialK = compute_special_k (Listx.from_list (all_tms :> nf list)) in
  let freshno = List.length var_names in
  let deltas =
   let dummy = `Var (max_int / 2, -666) in
    [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
- {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK=special_k; var_names; label}
+ {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label}
 ;;
 
 let problem_of ~div ~conv ~nums =