Moved parse' from Num to Parser

(cherry picked from commit 123d64bb5ae7127f6a51cbf44b63341de001a187)

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 c79cade6383dccc699c3ea591c6216237de477ff..355380eae032401af3518c89be84acc71a67a1f5 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -751,8 +751,8 @@ let append_zero =
 ;;
 
 let problem_of ~div ~conv ~nums =
- let all_tms = (match div with None -> [] | Some div -> print_endline(div);[div]) @ nums @ conv in
-  let all_tms, var_names = parse' all_tms in
+ 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, (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 c88fa8de1a666cd68cbb8d1e5c10286fd38157f5..f612def74371072024552c584be261a8ff01ea69 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -239,20 +239,6 @@ prerr_endline ("subst l:" ^ string_of_int l ^ " delift_by_one:" ^ string_of_bool
   aux 0 where
 ;;
 
-(************ Parsing ************************************)
-
-let parse' strs =
-  let fix_arity = function
-  | `I((n,_),args) -> `I((n,1+Listx.length args),args)
-  | _ -> assert false in
-  let rec aux = function
-  | Parser.Lam t -> `Lam (true, aux t)
-  | Parser.App (t1, t2) -> fix_arity (mk_app (aux t1) (aux t2))
-  | Parser.Var v -> `Var(v,1) in
-  let (tms, free) = Parser.parse_many strs in
-  List.map aux tms, free
-;;
-
 (************** Algorithm(s) ************************)
 
 let eta_compare x y =

diff --git a/ocaml/num.mli b/ocaml/num.mli
index 9cf81ccdd113e52d6162960d9edaff27de6c8648..c7b3256b15999aa31923db6325b316d63e21db81 100644 (file)
--- a/ocaml/num.mli
+++ b/ocaml/num.mli
@@ -40,7 +40,6 @@ val mk_appl : nf -> nf list -> nf
 val mk_appx : nf -> nf Listx.listx -> nf
 val mk_match : nf i_num_var_ -> 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..d21f4c2b07618ff03d879a0aaab89de011d658fd 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,26 @@ 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 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

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