Added problem wrongly backtracking

[fireball-separation.git] / ocaml / lambda4.ml

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index e5a09ec7c6eb06ba4d549f74cac46c26dd9d4bc0..7b669ca3789880e524c6d6870d1111a64999cfba 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -27,10 +27,14 @@ type problem =
  ; sigma: (int * nf) list (* the computed substitution *)
  ; deltas: discriminating_set ref list (* collection of all branches *)
  ; initialSpecialK: int
+ ; label : string
+ ; var_names : string list (* names of the original free variables *)
 
  ; trail: discriminating_set list list
 };;
 
+let label_of_problem {label} = label;;
+
 (* exceptions *)
 exception Pacman
 exception Bottom
@@ -75,7 +79,7 @@ let string_of_measure = string_of_int;;
 
 let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
  Console.print_hline ();
- prerr_string ("\n(* DISPLAY PROBLEM (" ^ label ^ ") - ");
+ prerr_string ("\n(* DISPLAY PROBLEM (" ^ p.label ^ " - " ^ label ^ ") ");
  let nl = "\n" in
  let deltas = String.concat (nl^"   ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
  let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
@@ -777,7 +781,8 @@ let solve (p, todo) =
 ;;
 
 let check p =
- (* check if there are duplicates in p.ps *)
+ (* TODO check if there are duplicates in p.ps
+     before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *)
  (* FIXME what about initial fragments? *)
  if (let rec f = function
      | [] -> false
@@ -797,62 +802,17 @@ let check p =
  else `Uncomplete
 ;;
 
-let zero = `Var(0,0);;
-
-let append_zero =
- function
-  | `I _
-  | `Var _ as i -> cast_to_i_n_var (mk_app i zero)
-  | `N _ -> raise (Parser.ParsingError " numbers in ps")
-;;
-
-let problem_of_2 (label, div, conv, nums, var_names) =
- (* DA SPOSTARE NEI TEST: *)
- let ps = List.map append_zero nums in (* crea lista applicando zeri o dummies *)
- let ps = sort_uniq ~compare:eta_compare (ps :> nf list) in
- let ps = List.map (cast_to_i_n_var) ps in
-
- (* 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 problem_of (label, div, conv, ps, var_names) =
+ (* TODO: replace div with bottom in problem??? *)
+ let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ ps @ conv in
+ if all_tms = [] then failwith "problem_of: 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 p = {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail} in
+ let sigma = [] in
+ let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK; trail; var_names; label} in
  p, check p
 ;;
-
-let problem_of ~div ~conv ~nums =
- let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in
- let all_tms, var_names = Parser.parse' all_tms in
- let div, (ps, conv) = match div with
-   | None -> None, list_cut (List.length nums, all_tms)
-   | Some _ -> Some (List.hd all_tms), list_cut (List.length nums, List.tl all_tms) in
-
- let div =
-  match div with
-   | None | Some `Bottom -> None
-   | Some (`I _ as t) -> Some t
-   | _ -> raise (Parser.ParsingError "div is not an inert or BOT in the initial problem") in
- let conv = Util.filter_map (
-  function
-  | #i_n_var as t -> Some t
-  | `Lam _ -> None
-  | _ -> raise (Parser.ParsingError "A term in conv is not i_n_var")
-  ) conv in
- let ps = List.map (
-  function
-   | #i_n_var as y -> y
-   | _ -> raise (Parser.ParsingError "A term in num is not i_n_var")
-  ) ps in
- problem_of_2("missing label", div, conv, ps, var_names)
-;;
-
-let problem_of_string_tmp s =
- let x = Parser.problem_of_string s in
- problem_of_2  x
-;;