-type term =\r
- | Var of int\r
- | App of term * term\r
- | Lam of term\r
-;;\r
-\r
-let mk_app x y = App(x, y);;\r
-let mk_lam x = Lam x;;\r
-let mk_var x = Var x;;\r
-\r
exception ParsingError of string;;\r
\r
+let mk_app x y = Num.mk_app x y;;\r
+let mk_lam x = `Lam(true, x);;\r
+let mk_var x = `Var(x, -666);;\r
+\r
let isAlphaNum c = let n = Char.code c in\r
(48 <= n && n <= 90) || (95 <= n && n <= 122) ;;\r
let isSpace c = c = ' ' || c = '\n' || c = '\t' ;;\r
\r
\r
**********************************************************************)\r
+\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 failwith "Example with `Bottom"\r
+ else if v = lev + n_pac then failwith "Example with `Pacman"\r
+ else if v = lev + n_bomb then failwith "Example with `Bomb"\r
+ else `Var(v,1) in (* 1 by default when variable not applied *)\r
+ (* Fix arity *)\r
+ let open Num in\r
+ let rec aux lev : nf -> nf = function\r
+ | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> aux lev t) args)\r
+ | `Var(n,_) -> fix lev n\r
+ | `Lam(_,t) -> `Lam (true, aux (lev+1) t)\r
+ | `Match _ | `N _ -> assert false in\r
+ List.map (aux 0) (tms :> Num.nf list), free\r
+;;\r
+\r
+let parse_problem s = failwith "TODO";\r