From 15c305b0d106b39616bdeea9aec9febc7539c2c1 Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 14 Jul 2017 19:25:23 +0200 Subject: [PATCH] problems now contain a label and the names of the original free variables --- ocaml/lambda4.ml | 14 ++++++-------- ocaml/lambda4.mli | 6 +++++- ocaml/parser.ml | 32 +++++++++++++++++++------------- 3 files changed, 30 insertions(+), 22 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index e5a09ec..bb78b22 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -27,6 +27,8 @@ type problem = ; sigma: (int * nf) list (* the computed substitution *) ; deltas: discriminating_set ref list (* collection of all branches *) ; initialSpecialK: int + ; label : string + ; var_names : string list (* names of the original free variables *) ; trail: discriminating_set list list };; @@ -806,7 +808,7 @@ let append_zero = | `N _ -> raise (Parser.ParsingError " numbers in ps") ;; -let problem_of_2 (label, div, conv, nums, var_names) = +let tmp (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 @@ -822,7 +824,8 @@ let problem_of_2 (label, div, conv, nums, var_names) = 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 + let sigma = [] in + let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK=special_k; trail; var_names; label} in p, check p ;; @@ -849,10 +852,5 @@ 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 - problem_of_2("missing label", div, conv, ps, var_names) -;; - -let problem_of_string_tmp s = - let x = Parser.problem_of_string s in - problem_of_2 x + tmp("missing label", div, conv, ps, var_names) ;; diff --git a/ocaml/lambda4.mli b/ocaml/lambda4.mli index ad6ca7e..bbfd13b 100644 --- a/ocaml/lambda4.mli +++ b/ocaml/lambda4.mli @@ -15,5 +15,9 @@ 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 tmp: (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 *)) -> problem * response val solve: problem * response -> result diff --git a/ocaml/parser.ml b/ocaml/parser.ml index 61dbf83..ac69251 100644 --- a/ocaml/parser.ml +++ b/ocaml/parser.ml @@ -171,22 +171,29 @@ let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j") ;; let problem_of_string s = +prerr_endline (s); let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in + let lines = List.map String.trim lines 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 aux (last, 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 + if line = "" then chr, name, div, conv, ps else + let rec aux' chr line = + if chr = "#" + then chr, line, div, conv, ps + else if chr = "D" + then chr, name, line, conv, ps + else if chr = "C" + then chr, name, div, line::conv, ps + else if chr = "N" + then chr, name, div, conv, line::ps + else if last = "" + then raise (ParsingError ("Unexpected at beginning of problem: " ^ chr)) + else aux' last (chr ^ line) in + aux' chr line 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 @@ -235,8 +242,7 @@ let conv = Util.filter_map ( let ps = List.map ( function | #i_n_var as y -> y - | _ -> raise (ParsingError "A term in num is not i_n_var") + | _ as y -> raise (ParsingError ("A term in num is not i_n_var" ^ Num.string_of_nf y)) ) ps in - name, div, conv, ps, free ;; -- 2.39.2