First draft of Parser.problem_of_string

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index fa9b043e4f64d1b60bed908a2893f83389d4585c..0db3c16707994d8f45ba925758da2c14ee0169a0 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -747,6 +747,24 @@ let append_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 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
+ {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}
+;;
+
 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
@@ -770,19 +788,10 @@ 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
- (* DA SPOSTARE NEI TEST: *)
- let ps = List.map append_zero ps 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??? *)
+ problem_of_2("missing label", div, conv, ps, var_names)
+;;
 
- let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *)
- 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 p = {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k} in
- p
+let problem_of_string_tmp s =
+ let x = Parser.problem_of_string s in
+ problem_of_2  x
 ;;