; sigma: (int * nf) list (* the computed substitution *)
; deltas: (int * nf) list ref list (* collection of all branches *)
; initialSpecialK: int
+ ; label : string
+ ; var_names : string list (* names of the original free variables *)
};;
let all_terms p =
| `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
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}
+ {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK=special_k; var_names; label}
;;
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)
;;