Moved parse' from Num to Parser

diff --git a/ocaml/Makefile b/ocaml/Makefile
index 198855fa5805d3833b5ddf88881fd17350c30773..430f1596fa5f6c5c529f15c4a32c3350276913c9 100644 (file)
--- a/ocaml/Makefile
+++ b/ocaml/Makefile
@@ -1,6 +1,6 @@
 OCAMLC = ocamlopt -g -rectypes
 LIB = unix.cmxa str.cmxa
-UTILS = util.cmx parser.cmx console.cmx listx.cmx pure.cmx num.cmx
+UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx
 
 all: a.out test4.out
        # test.out

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index ed43936638020efe31958242c0edd27b11834f60..b0e4bc94cdfe83a9aaeb275fece6e0a11dc64f43 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -790,7 +790,7 @@ let append_zero =
 
 let problem_of ~div ~conv ~nums =
  let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in
-  let all_tms, var_names = parse' all_tms in
+ let all_tms, var_names = Parser.parse' all_tms in
   let div, (tms, 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

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 82c4b3803e4a0868e6e96eb58d935b9cae146628..d9cdf379857957bae4a871fd6b119f300f3056eb 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -266,28 +266,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool
 
 (************ Parsing ************************************)
 
-let parse' strs =
-  let fix_arity = function
-   | `I((n,_),args) -> `I((n,1+Listx.length args),args)
-   | _ -> assert false in
-  let (tms, free) = Parser.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 rec aux lev = function
-   | Parser.Lam t -> `Lam (true, aux (lev+1) t)
-   | Parser.App (t1, t2) -> fix_arity (mk_app (aux lev t1) (aux lev t2))
-   | Parser.Var v -> fix lev v in
-  List.map (aux 0) tms, free
-;;
-
 (************** Algorithm(s) ************************)
 
 let eta_compare x y =

diff --git a/ocaml/num.mli b/ocaml/num.mli
index 6de26456cb1aa8d2c990e2beeaea3d779b34bc5a..33ea10fee01f5530e904fb10940efc77ba50d07b 100644 (file)
--- a/ocaml/num.mli
+++ b/ocaml/num.mli
@@ -34,7 +34,6 @@ val mk_appl : nf -> nf list -> nf
 val mk_appx : nf -> nf Listx.listx -> nf
 val mk_match : nf -> var -> int -> (int * nf) list ref -> nf list -> nf
 val subst : bool -> bool -> int -> nf -> nf -> nf
-val parse' : string list -> nf list * string list
 val eta_compare : nf -> nf -> int
 val eta_eq : [< nf ] -> [< nf ] -> bool
 val eta_subterm : [< nf ] -> [< nf ] -> bool

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index b496070b690e9077d6b482774f06d0a8ab1c776b..d7a1b36d31d3dd30d0f8d63f8f2182ff93f22a0d 100644 (file)
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -1,15 +1,9 @@
-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
@@ -147,3 +141,33 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
 \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 `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

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index c073c3af1a7436e537381ea6b88b234a5735dc49..c205cb293640fc6ef7c40e287971547cc722a113 100644 (file)
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,9 +1,10 @@
-type term =\r
-  | Var of int\r
-  | App of term * term\r
-  | Lam of term\r
+exception ParsingError of string\r
 \r
 (* parses a string to a term *)\r
-val parse: string -> term\r
+(* val parse: string -> Num.nf *)\r
 (* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)\r
-val parse_many: string list -> term list * string list\r
+val parse_many: string list -> Num.nf list * string list\r
+val parse': string list -> Num.nf list * string list\r
+val parse_problem:\r
+ string ->\r
+  Num.i_var option * Num.i_n_var list * Num.i_n_var list\r