From: acondolu Date: Fri, 14 Jul 2017 16:02:19 +0000 (+0200) Subject: First draft of Parser.problem_of_string X-Git-Tag: weak-reduction-separation~37 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b3b3eb5c68d4b1ca28ef911b81e6757db080187;p=fireball-separation.git 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 fa9b043..0db3c16 100644 --- 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 d8148d5..4af5060 100644 --- a/ocaml/lambda4.mli +++ b/ocaml/lambda4.mli @@ -6,4 +6,6 @@ type result = [ ] val problem_of: div:(string option) -> conv:string list -> nums:string list -> problem +(* the following will soon replace the one above *) +val problem_of_string_tmp: string -> problem val solve: problem -> result diff --git a/ocaml/parser.ml b/ocaml/parser.ml index d21f4c2..47c50d4 100644 --- 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 ;; -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 assert false + else if v = lev + n_pac then assert false + else if v = lev + n_bomb then assert false + else `Var(v,1) in (* 1 by default when variable not applied *) + (* Fix arity *) + let open Num in + let rec aux lev : nf -> nf = function + | `I((n,_), args) -> `I((n,1 + Listx.length args), Listx.map (fun t -> aux lev t) args) + | `Var(n,_) -> fix lev n + | `Lam(_,t) -> `Lam (true, aux (lev+1) t) + | `Match _ | `N _ -> 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 + 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 *)