]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Failure in case of empty problem, to be fixed
authoracondolu <andrea.condoluci@unibo.it>
Fri, 14 Jul 2017 17:39:21 +0000 (19:39 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Fri, 14 Jul 2017 17:39:21 +0000 (19:39 +0200)
ocaml/lambda4.ml

index bb78b2278d5ff3aeb5b0751da090899bd322e418..ce0663a05da2714b8e59f8a2734e5aa2a8c10b82 100644 (file)
@@ -816,16 +816,16 @@ 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
  let trail = [] in
  let sigma = [] in
- let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK=special_k; trail; var_names; label} in
+ let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK; trail; var_names; label} in
  p, check p
 ;;