From 8b69a4c59242b64294c7065a4e85437ce3cbc32d Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 14 Jul 2017 18:02:19 +0200 Subject: [PATCH] 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 --- ocaml/lambda4.ml | 40 ++++++++++++++++---------- ocaml/lambda4.mli | 2 ++ ocaml/parser.ml | 71 ++++++++++++++++++++++++++++++++++++++++++++++- ocaml/parser.mli | 12 ++++---- 4 files changed, 103 insertions(+), 22 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 5422704..e5a09ec 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -806,6 +806,26 @@ 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 + let trail = [] in + let p = {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail} in + p, check p +;; + 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 @@ -829,20 +849,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 trail = [] in - let p = {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k; trail} in - p, check 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 0b92ad9..ad6ca7e 100644 --- a/ocaml/lambda4.mli +++ b/ocaml/lambda4.mli @@ -14,4 +14,6 @@ type result = [ ] val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem * response +(* the following will soon replace the one above *) +val problem_of_string_tmp: string -> problem * response val solve: problem * response -> result diff --git a/ocaml/parser.ml b/ocaml/parser.ml index d7a1b36..61dbf83 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -170,4 +170,73 @@ 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 ;; -let parse_problem s = failwith "TODO"; +let problem_of_string s = + let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in + let lines = List.filter ((<>) "") lines in + prerr_endline("number of lines" ^ string_of_int (List.length lines)); + let aux (name, div, conv, ps) line = + let chr = String.sub line 0 1 in + let line = String.sub line 1 (String.length line - 1) in + if chr = ":" + then line, div, conv, ps + else if chr = "D" + then name, line, conv, ps + else if chr = "C" + then name, div, line::conv, ps + else if chr = "N" + then name, div, conv, line::ps + else raise (ParsingError ("Unexpected at beginning of line: " ^ chr)) in + let name, div, conv, ps = List.fold_left aux ("?", "", [], []) lines in + let div_provided = div <> "" in + let div = if div_provided then div else "BOT" in + let strs = [div] @ ps @ conv in + + (* parse' *) + 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 -> `Pacman + and aux lev : Num.nf -> Num.nf = function + | #nf_nob as t -> aux_nob lev t + | `Bottom -> assert false in +let all_tms = List.map (aux 0) (tms :> Num.nf list) in + +(* problem_of *) +let div, (ps, conv) = List.hd all_tms, Util.list_cut (List.length ps, List.tl all_tms) in + +let div = if not div_provided || div = `Bottom + then None + else match div with + | `I _ as t -> Some t + | _ -> raise (ParsingError "div is not an inert or BOT in the initial problem") in +let conv = Util.filter_map ( + function + | #i_n_var as t -> Some t + | `Lam _ -> None + | _ -> raise (ParsingError "A term in conv is not i_n_var") + ) conv in +let ps = List.map ( + function + | #i_n_var as y -> y + | _ -> raise (ParsingError "A term in num is not i_n_var") + ) ps in + + name, div, conv, ps, free +;; diff --git a/ocaml/parser.mli b/ocaml/parser.mli index c205cb2..9275067 100644 --- a/ocaml/parser.mli +++ b/ocaml/parser.mli @@ -1,10 +1,10 @@ exception ParsingError of string -(* parses a string to a term *) -(* val parse: string -> Num.nf *) -(* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *) -val parse_many: string list -> Num.nf list * string list val parse': string list -> Num.nf list * string list -val parse_problem: +val problem_of_string: string -> - Num.i_var option * Num.i_n_var list * Num.i_n_var list + string (* problem label *) + * Num.i_var option (* div *) + * Num.i_n_var list (* conv *) + * Num.i_n_var list (* ps *) + * string list (* names of free variables *) -- 2.39.2