-
-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)
-;;