X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fparser.ml;h=d7a1b36d31d3dd30d0f8d63f8f2182ff93f22a0d;hb=123d64bb5ae7127f6a51cbf44b63341de001a187;hp=90cda05bd2313d661d51c009919eccdf9c1407cd;hpb=bfd8f8a98a7392ac8cbd9070a8e4ff4d06e09510;p=fireball-separation.git

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index 90cda05..d7a1b36 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -1,30 +1,19 @@
-type term =
-  | Var of int
-  | App of term * term
-  | Lam of term
-;;
-
-let mk_app x y = App(x, y);;
-let mk_lam x = Lam x;;
-let mk_var x = Var x;;
-
 exception ParsingError of string;;
 
+let mk_app x y = Num.mk_app x y;;
+let mk_lam x = `Lam(true, x);;
+let mk_var x = `Var(x, -666);;
+
 let isAlphaNum c = let n = Char.code c in
  (48 <= n && n <= 90) || (95 <= n && n <= 122) ;;
 let isSpace c = c = ' ' || c = '\n' || c = '\t' ;;
 
-let rec index_of x =
-  function
-  | [] -> raise (Failure "index_of: Not Found")
-  | h::t -> if x = h then 0 else 1 + index_of x t
-;;
 (* FIXME *)
 let mk_var' (bound, free) x =
   if List.mem x bound
-  then free, mk_var (index_of x bound)
+  then free, mk_var (Util.index_of x bound)
   else if List.mem x free
-       then free, mk_var (List.length bound + index_of x free)
+       then free, mk_var (List.length bound + Util.index_of x free)
        else (free @ [x]), mk_var (List.length bound + List.length free)
 ;;
 
@@ -152,3 +141,33 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
 
 
 **********************************************************************)
+
+ let parse' strs =
+   let (tms, free) = parse_many strs in
+   (* Replace pacmans and bottoms *)
+   let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in
+   let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in
+   let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in
+   let fix lev v =
+    if v = lev + n_bot then `Bottom
+     else if v = lev + n_pac then `Pacman
+      else if v = lev + n_bomb then `Lam(true, `Bottom)
+       else `Var(v,1) in (* 1 by default when variable not applied *)
+   (* Fix arity *)
+   let open Num in
+   let exclude_bottom = function
+   | #nf_nob as t -> t
+   | `Bottom -> raise (ParsingError "Input term not in normal form") in
+   let rec aux_nob lev : nf_nob -> nf = function
+   | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> exclude_bottom (aux_nob lev t)) args)
+   | `Var(n,_) -> fix lev n
+   | `Lam(_,t) -> `Lam (true, aux (lev+1) t)
+   | `Match _ | `N _ -> assert false
+   | `Pacman -> assert false
+   and aux lev : Num.nf -> Num.nf = function
+    | #nf_nob as t -> aux_nob lev t
+    | `Bottom -> assert false in
+ List.map (aux 0) (tms :> Num.nf list), free
+;;
+
+let parse_problem s = failwith "TODO";