problems now contain a label and the names of the original free variables

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index e5a09ec7c6eb06ba4d549f74cac46c26dd9d4bc0..bb78b2278d5ff3aeb5b0751da090899bd322e418 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -27,6 +27,8 @@ 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
 };;
@@ -806,7 +808,7 @@ let append_zero =
   | `N _ -> raise (Parser.ParsingError " numbers in ps")
 ;;
 
-let problem_of_2 (label, div, conv, nums, var_names) =
+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
@@ -822,7 +824,8 @@ let problem_of_2 (label, div, conv, nums, var_names) =
   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=special_k; trail; var_names; label} in
  p, check p
 ;;
 
@@ -849,10 +852,5 @@ let problem_of ~div ~conv ~nums =
    | #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
+ tmp("missing label", div, conv, ps, var_names)
 ;;