]
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
`Separable p_finale.sigma
;;
-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 =
[ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
{freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label}
;;
-
-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 -> 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)
-;;