First draft of Parser.problem_of_string

- problem_of_string should unify old Lambda4.problem_of and Parser.parse'
- Lambda4.problem_of was temporarily factored in problem_of_2
  and problem_of_String_tmp

(cherry picked from commit 8b69a4c59242b64294c7065a4e85437ce3cbc32d)

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index fa9b043e4f64d1b60bed908a2893f83389d4585c..0db3c16707994d8f45ba925758da2c14ee0169a0 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -747,6 +747,24 @@ let append_zero =
   | `N _ -> raise (Parser.ParsingError " numbers in ps")
 ;;
 
+let problem_of_2 (label, div, conv, nums, var_names) =
+ (* DA SPOSTARE NEI TEST: *)
+ let ps = List.map append_zero nums in (* crea lista applicando zeri o dummies *)
+ let ps = sort_uniq ~compare:eta_compare (ps :> nf list) in
+ let ps = List.map (cast_to_i_n_var) ps in
+
+ (* TODO: *)
+ (* replace div with bottom in problem??? *)
+ let special_k =
+  let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
+  compute_special_k (Listx.from_list (all_tms :> nf list)) in (* compute initial special K *)
+ let freshno = List.length var_names in
+ let deltas =
+  let dummy = `Var (max_int / 2, -666) in
+   [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
+ {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}
+;;
+
 let problem_of ~div ~conv ~nums =
  let all_tms = (match div with None -> [] | Some div -> [div]) @ nums @ conv in
  let all_tms, var_names = Parser.parse' all_tms in
@@ -770,19 +788,10 @@ let problem_of ~div ~conv ~nums =
    | #i_n_var as y -> y
    | _ -> raise (Parser.ParsingError "A term in num is not i_n_var")
   ) ps in
- (* DA SPOSTARE NEI TEST: *)
- let ps = List.map append_zero ps in (* crea lista applicando zeri o dummies *)
- let ps = sort_uniq ~compare:eta_compare (ps :> nf list) in
- let ps = List.map (cast_to_i_n_var) ps in
-
- (* TODO: *)
- (* replace div with bottom in problem??? *)
+ problem_of_2("missing label", div, conv, ps, var_names)
+;;
 
- let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *)
- let freshno = List.length var_names in
- let deltas =
-  let dummy = `Var (max_int / 2, -666) in
-   [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
- let p = {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k} in
- p
+let problem_of_string_tmp s =
+ let x = Parser.problem_of_string s in
+ problem_of_2  x
 ;;

diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli
index d8148d5399aea9ba3d3ac582506f0dea47eace94..4af50606788f0f79e8f54b9b6742fc2e2ef35b0c 100644 (file)
--- a/ocaml/lambda4.mli
+++ b/ocaml/lambda4.mli
@@ -6,4 +6,6 @@ type result = [
 ]\r
 \r
 val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem\r
+(* the following will soon replace the one above *)\r
+val problem_of_string_tmp: string -> problem\r
 val solve: problem -> result\r

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index d21f4c2b07618ff03d879a0aaab89de011d658fd..47c50d486538a72d48a5d924d0e9dd8ec6404d79 100644 (file)
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -163,4 +163,66 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j")
  List.map (aux 0) (tms :> Num.nf list), free\r
 ;;\r
 \r
-let parse_problem s = failwith "TODO";\r
+let problem_of_string s =\r
+ let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in\r
+ let lines = List.filter ((<>) "") lines in\r
+ prerr_endline("number of lines" ^ string_of_int (List.length lines));\r
+ let aux (name, div, conv, ps) line =\r
+  let chr = String.sub line 0 1 in\r
+  let line = String.sub line 1 (String.length line - 1) in\r
+  if chr = ":"\r
+   then line, div, conv, ps\r
+  else if chr = "D"\r
+   then name, line, conv, ps\r
+  else if chr = "C"\r
+   then name, div, line::conv, ps\r
+  else if chr = "N"\r
+   then name, div, conv, line::ps\r
+  else raise (ParsingError ("Unexpected at beginning of line: " ^ chr)) in\r
+ let name, div, conv, ps = List.fold_left aux ("?", "", [], []) lines in\r
+ let div_provided = div <> "" in\r
+ let div = if div_provided then div else "BOT" in\r
+ let strs = [div] @ ps @ conv in\r
+\r
+ (* parse' *)\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 assert false\r
+   else if v = lev + n_pac then assert false\r
+    else if v = lev + n_bomb then assert false\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
+let all_tms = List.map (aux 0) (tms :> Num.nf list) in\r
+\r
+(* problem_of *)\r
+let div, (ps, conv) = List.hd all_tms, Util.list_cut (List.length ps, List.tl all_tms) in\r
+\r
+let div = if not div_provided\r
+ then None\r
+ else match div with\r
+  | `I _ as t -> Some t\r
+  | _ -> raise (ParsingError "div is not an inert or BOT in the initial problem") in\r
+let conv = Util.filter_map (\r
+ function\r
+ | #i_n_var as t -> Some t\r
+ | `Lam _ -> None\r
+ | _ -> raise (ParsingError "A term in conv is not i_n_var")\r
+ ) conv in\r
+let ps = List.map (\r
+ function\r
+  | #i_n_var as y -> y\r
+  | _ -> raise (ParsingError "A term in num is not i_n_var")\r
+ ) ps in\r
+\r
+ name, div, conv, ps, free\r
+;;\r

diff --git a/ocaml/parser.mli b/ocaml/parser.mli
index c205cb293640fc6ef7c40e287971547cc722a113..927506732d13e8c125769d28a4c3dcaf5696c6af 100644 (file)
--- a/ocaml/parser.mli
+++ b/ocaml/parser.mli
@@ -1,10 +1,10 @@
 exception ParsingError of string\r
 \r
-(* parses a string to a 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 -> Num.nf list * string list\r
 val parse': string list -> Num.nf list * string list\r
-val parse_problem:\r
+val problem_of_string:\r
  string ->\r
-  Num.i_var option * Num.i_n_var list * Num.i_n_var list\r
+  string (* problem label *)\r
+  * Num.i_var option (* div *)\r
+  * Num.i_n_var list (* conv *)\r
+  * Num.i_n_var list (* ps *)\r
+  * string list (* names of free variables *)\r