Important: added special variable "Z" for zero.

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 02ac1e018ff96f1cb1d9cacb8e85dc58be733adb..7b669ca3789880e524c6d6870d1111a64999cfba 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -781,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
@@ -801,25 +802,10 @@ 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 tmp (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 all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
- if all_tms = [] then failwith "FIXME: empty problem";
+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 =
@@ -830,29 +816,3 @@ let tmp (label, div, conv, nums, var_names) =
  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
- tmp("missing label", div, conv, ps, var_names)
-;;