+\r
+ let parse' strs =\r
+ let (tms, free) = parse_many strs in\r
+ (* Replace pacmans and bottoms *)\r
+ let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in\r
+ let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in\r
+ let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in\r
+ let fix lev v =\r
+ if v = lev + n_bot then `Bottom\r
+ else if v = lev + n_pac then `Pacman\r
+ else if v = lev + n_bomb then `Lam(true, `Bottom)\r
+ else `Var(v,1) in (* 1 by default when variable not applied *)\r
+ (* Fix arity *)\r
+ let open Num in\r
+ let exclude_bottom = function\r
+ | #nf_nob as t -> t\r
+ | `Bottom -> raise (ParsingError "Input term not in normal form") in\r
+ let rec aux_nob lev : nf_nob -> nf = function\r
+ | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args)\r
+ | `Var(n,_) -> fix lev n\r
+ | `Lam(_,t) -> `Lam (true, aux (lev+1) t)\r
+ | `Match _ | `N _ -> assert false\r
+ | `Pacman -> assert false\r
+ and aux lev : Num.nf -> Num.nf = function\r
+ | #nf_nob as t -> aux_nob lev t\r
+ | `Bottom -> assert false in\r
+ List.map (aux 0) (tms :> Num.nf list), free\r
+;;\r
+\r
+let parse_problem s = failwith "TODO";\r