From f1873841a3271d332cb8429b46e7bc7e0bca2402 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 31 May 2018 23:38:31 +0200 Subject: [PATCH] Updated simple with current parser - Removed parser_andrea - Generalized problems.ml - Moved sample problems from simple.ml to problems/simple.0 --- ocaml/Makefile | 4 +- ocaml/lambda4.ml | 11 ++ ocaml/parser_andrea.ml | 266 ---------------------------------------- ocaml/parser_andrea.mli | 25 ---- ocaml/problems.ml | 28 ++--- ocaml/problems.mli | 4 + ocaml/problems/simple.0 | 46 +++++++ ocaml/simple.ml | 66 +++------- ocaml/simple.mli | 9 +- ocaml/simple_test.ml | 5 +- 10 files changed, 95 insertions(+), 369 deletions(-) delete mode 100644 ocaml/parser_andrea.ml delete mode 100644 ocaml/parser_andrea.mli create mode 100644 ocaml/problems/simple.0 diff --git a/ocaml/Makefile b/ocaml/Makefile index fae0449..3a94a7a 100644 --- a/ocaml/Makefile +++ b/ocaml/Makefile @@ -1,13 +1,13 @@ OCAMLC = ocamlopt -g -rectypes LIB = unix.cmxa str.cmxa -UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx parser_andrea.cmx +UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx problems.cmx all: a.out test4.out simple.out simple_test.out run: test4.out bash run -a.out: $(UTILS) lambda4.cmx problems.cmx +a.out: $(UTILS) lambda4.cmx $(OCAMLC) -o a.out $(LIB) $^ test4.out: $(UTILS) lambda4.cmx test.ml diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 9395daa..90a91e0 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -719,3 +719,14 @@ let problem_of (label, div, conv, ps, var_names) = [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in {freshno; div; conv; ps; sigma=[]; deltas; initialSpecialK; var_names; label} ;; + +(* assert_depends solves the problem, and checks if the result was expected *) +let assert_depends x = + let c = String.sub (label_of_problem x) 0 1 in + match solve x with + | `Unseparable s when c = "!" -> + failwith ("assert_depends: unseparable because: " ^ s ^ ".") + | `Separable _ when c = "?" -> + failwith ("assert_depends: separable.") + | _ -> () in +Problems.main (assert_depends ++ problem_of); diff --git a/ocaml/parser_andrea.ml b/ocaml/parser_andrea.ml deleted file mode 100644 index fbce730..0000000 --- a/ocaml/parser_andrea.ml +++ /dev/null @@ -1,266 +0,0 @@ -type term = - | Var of int - | App of term * term - | Lam of term -;; - -let mk_app x y = App(x, y);; -let mk_lam x = Lam x;; -let mk_var x = Var x;; - -exception ParsingError of string;; - -let isAlphaNum c = let n = Char.code c in - (48 <= n && n <= 90) || (95 <= n && n <= 122) ;; -let isSpace c = c = ' ' || c = '\n' || c = '\t' ;; - -(* FIXME *) -let mk_var' (bound, free) x = - if x <> "@" && List.mem x bound - then free, mk_var (Util.index_of x bound) - else if x <> "@" && List.mem x free - then free, mk_var (List.length bound + Util.index_of x free) - else (free @ [x]), mk_var (List.length bound + List.length free) -;; - -let mk_app' = function - | [] -> assert false - | t :: ts -> List.fold_left mk_app t ts -;; - -let explode s = - let len = String.length s in - let rec aux i l = - if i >= len || s.[i] = '#' then l else aux (i+1) (s.[i] :: l) - in List.rev (aux 0 []) -;; - -let implode l = - let res = String.create (List.length l) in - let rec aux i = function - | [] -> res - | c :: l -> String.set res i c; aux (i + 1) l in - aux 0 l -;; - -let rec strip_spaces = function - | c::cs when isSpace c -> strip_spaces cs - | cs -> cs -;; - -let read_var s = - let rec aux = function - | [] -> None, [] - | c::cs as x -> - if c = '@' then - (if cs <> [] && (let hd = List.hd cs in hd = '@' || isAlphaNum hd) - then raise (ParsingError ("Unexpected `"^String.make 1 (List.hd cs)^"` after `@`.")) - else Some['@'], cs) - else if isAlphaNum c - then match aux cs with - | (Some x), cs' -> Some (c :: x), cs' - | None, cs' -> (Some [c]), cs' - else None, x - in match aux s with - | None, y -> None, y - | Some x, y -> Some (implode x), y -;; - -let read_var' (bound, free as vars) s = - match read_var s with - | Some varname, cs -> - let free, v = mk_var' vars varname in - Some [v], cs, (bound, free) - | None, _ -> raise (ParsingError ("Can't read variable")) -;; - -let rec read_smt vars = - let check_if_lambda cs = match read_var cs with - | None, _ -> false - | Some x, cs -> match strip_spaces cs with - | [] -> false - | c::_ -> c = '.' - in let read_lambda (bound, free) cs = ( - match read_var (strip_spaces cs) with - | Some varname, cs -> - let vars' = (varname::bound, free) in - (match strip_spaces cs with - | [] -> raise (ParsingError "Lambda expression incomplete") - | c::cs -> (if c = '.' then (match read_smt vars' cs with - | None, _, _ -> raise (ParsingError "Lambda body expected") - | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free) - | Some _, _, _ -> assert false - ) else raise (ParsingError "Expected `.` after variable in lambda") - )) - | _, _ -> assert false - ) in let rec aux vars cs = - match strip_spaces cs with - | [] -> None, [], vars - | c::_ as x -> - let tms, cs, vars = ( - if c = '(' then read_pars vars x - else if c = ')' then (None, x, vars) - else if check_if_lambda x then read_lambda vars x - else read_var' vars x) in - match tms with - | Some [tm] -> ( - match aux vars cs with - | None, cs, vars -> Some [tm], cs, vars - | Some ts, cs, vars -> Some (tm :: ts), cs, vars - ) - | Some _ -> assert false - | None -> None, x, vars - in fun cs -> match aux vars cs with - | None, cs, vars -> None, cs, vars - | Some ts, cs, vars -> Some [mk_app' ts], cs, vars -and read_pars vars = function - | [] -> None, [], vars - | c::cs -> if c = '(' then ( - let tm, cs, vars = read_smt vars cs in - let cs = strip_spaces cs in - match cs with - | [] -> None, [], vars - | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError "Missing `)`") - ) else assert false -;; - -let parse x = - match read_smt ([],[]) (explode x) with - | Some [y], [], _ -> y - | _, _, _ -> assert false -;; - -let parse_many strs = - let f (x, y) z = match read_smt y (explode z) with - | Some[tm], [], vars -> (tm :: x, vars) - | _, _, _ -> assert false - in let aux = List.fold_left f ([], ([], [])) - in let (tms, (_, free)) = aux strs - in (List.rev tms, free) -;; - -(********************************************************************** - -let rec string_of_term = function - | Tvar n -> string_of_int n - | Tapp(t1, t2) -> "(" ^ string_of_term t1 ^ " " ^ string_of_term t2 ^ ")" - | Tlam(t1) -> "(\\" ^ string_of_term t1 ^ ")" -;; - -let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j"));; - - -*******************************************************************************) - -(* let problem_of_string s = - let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in - let head, lines = List.hd lines, List.tl lines in - let name = String.trim (String.sub head 1 (String.length head - 1)) in - let lines = List.filter ((<>) "") lines in - let aux (last, div, conv, ps) line = - let chr = String.sub line 0 1 in - let line = String.trim (String.sub line 1 (String.length line - 1)) in - if line = "" then chr, div, conv, ps else - let rec aux' chr line = - if chr = "#" - then chr, div, conv, ps - else if chr = "D" - then chr, line, conv, ps - else if chr = "C" - then chr, div, line::conv, ps - else if chr = "N" - then chr, div, conv, line::ps - else if chr = " " - then aux' last line - else raise (ParsingError - ("Unexpected at beginning of problem: `" ^ chr ^ "` " ^ line)) in - aux' chr line in - let _, 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 - - if List.length ps = 0 && List.length conv = 0 - then raise (ParsingError "Parsed empty problem"); - - (* 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 if v = lev then `Var(v, min_int) (* zero *) - 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 - (* actually, the following may be assert false *) - | `Bottom -> raise (ParsingError "Input term not in normal form") in - let rec aux_nob lev : nf_nob -> nf = function - | `I((n,_), args) -> `I((n,(if lev = 0 then 0 else 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 "D is not an inert in the initial problem") in -let conv = Util.filter_map ( - function - | #i_n_var as t -> Some t - | `Lam _ -> None - | _ -> raise (ParsingError "A C-term is not i_n_var") - ) conv in -let ps = List.map ( - function - | #i_n_var as y -> y - | _ -> raise (ParsingError "An N-term is not i_n_var") - ) ps in - name, div, conv, ps, free -;; - - -let from_file path = - let lines = ref ["#"] in - let chan = open_in path in - let _ = try - while true; do - lines := input_line chan :: !lines - done - with End_of_file -> - close_in chan in - let txt = String.concat "\n" (List.rev !lines) in - let problems = Str.split (Str.regexp "[\n\r]+\\$") txt in - List.map problem_of_string (List.tl (List.map ((^) "$") problems)) -;; *) - -let parse x = - match read_smt ([],[]) (explode x) with - | Some [y], [], _ -> y - | _, _, _ -> assert false -;; - - -let parse_many strs = - let f (x, y) z = match read_smt y (explode z) with - | Some[tm], [], vars -> (tm :: x, vars) - | _, _, _ -> assert false - in let aux = List.fold_left f ([], ([], [])) - in let (tms, (_, free)) = aux strs - in (List.rev tms, free) -;; diff --git a/ocaml/parser_andrea.mli b/ocaml/parser_andrea.mli deleted file mode 100644 index 8dba854..0000000 --- a/ocaml/parser_andrea.mli +++ /dev/null @@ -1,25 +0,0 @@ -type term = - | Var of int - | App of term * term - | Lam of term - -exception ParsingError of string - -(* val problem_of_string: - string -> - 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 *) -val from_file : string -> - (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 *)) list *) - - (* parses a string to a term *) - val parse: string -> term - (* 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 -> term list * string list diff --git a/ocaml/problems.ml b/ocaml/problems.ml index 9ff4778..28edceb 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -1,4 +1,3 @@ -open Lambda4;; open Util;; (* Syntax for problem files in problem/ folder: @@ -17,23 +16,12 @@ open Util;; *) -(* assert_depends solves the problem, and checks if the result was expected *) -let assert_depends x = - let c = String.sub (label_of_problem x) 0 1 in - match solve x with - | `Unseparable s when c = "!" -> - failwith ("assert_depends: unseparable because: " ^ s ^ ".") - | `Separable _ when c = "?" -> - failwith ("assert_depends: separable.") - | _ -> () -;; - -(* TODO *) -(* div under a lambda in conv *) - -if Array.length Sys.argv = 1 - then failwith "no command line args. Please use e.g. ./a.out problems/*" -else Array.iteri (fun i filename -> if i > 0 then - List.iter (assert_depends ++ problem_of) (Parser.from_file filename) - ) Sys.argv +let main f = + print_endline Sys.executable_name; + try ignore (Str.search_forward (Str.regexp_string "test") Sys.executable_name 0) + with Not_found -> + (if Array.length Sys.argv = 1 + then failwith "no command line args. Please use e.g. ./cmd.out problems/*" + else Array.iteri (fun i filename -> if i > 0 then + List.iter f (Parser.from_file filename)) Sys.argv) ;; diff --git a/ocaml/problems.mli b/ocaml/problems.mli index e69de29..5315cc7 100644 --- a/ocaml/problems.mli +++ b/ocaml/problems.mli @@ -0,0 +1,4 @@ +val main : + (string * Num.i_var option * Num.i_n_var list * Num.i_n_var list * + string list -> unit) -> + unit diff --git a/ocaml/problems/simple.0 b/ocaml/problems/simple.0 new file mode 100644 index 0000000..4942099 --- /dev/null +++ b/ocaml/problems/simple.0 @@ -0,0 +1,46 @@ +$ simple.0/0 +D x x +C x y +C y y +C y x + +$ simple.0/1 +D x y +C x (_. x) +C y z +C y x + +$ simple.0/2 +D a (x. x b) (x. x c) +C a (x. b b) @ +C a @ c +C a (x. x x) a +C a (a a a) (a c c) + +$ simple.0/3 +D x (y. x y y) +C x (y. x y x) + +$ simple.0/4 +D x a a a a +C x b a a a +C x a b a a +C x a a b a +C x a a a b + +$ simple.0/5 +# Controesempio ad usare un conto dei lambda che non considera le permutazioni +D x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b +C x a a a a (_. a) b b b +C x a a a a (_. _. _. _. x. y. x y) + +$ simple.0/6 +# bug in eat that was erasing terms in convergent that then diverged +D x y z +C x @ @ +C z (y @ (y @)) + +$ simple.0/7 +# bug in no_leading_lambdas where x in j-th position +D v0 (v1 v2) (x. y. v0 v3 v4 v2) +C v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8))) diff --git a/ocaml/simple.ml b/ocaml/simple.ml index efa5c25..991779e 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -287,19 +287,10 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")") let p = subst_in_problem subst p in sanity p ;; -;; -let parse strs = - let rec aux level = function - | Parser_andrea.Lam t -> L (aux (level + 1) t) - | Parser_andrea.App (t1, t2) -> - if level = 0 then mk_app (aux level t1) (aux level t2) - else A(aux level t1, aux level t2) - | Parser_andrea.Var v -> V v in - let (tms, free) = Parser_andrea.parse_many strs in - (List.map (aux 0) tms, free) ;; + let rec auto p = let hd_var, n_args = get_inert p.div in match get_subterm_with_head_and_args hd_var n_args p.conv with @@ -320,13 +311,20 @@ let rec auto p = auto p ;; -let problem_of div convs = - let rec conv_join = function - | [] -> "@" - | x::xs -> conv_join xs ^ " ("^ x ^")" in +let problem_of (label, div, convs, ps, var_names) = print_hline (); - let conv = conv_join convs in - let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in + let rec aux = function + | `Lam(_, t) -> L (aux t) + | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app x (aux y)) (V v) args + | `Var(v,_) -> V v + | `N _ | `Match _ -> assert false in + assert (List.length ps = 0); + let convs = List.rev convs in + let conv = List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) convs in + let var_names = "@" :: var_names in + let div = match div with + | Some div -> aux (div :> Num.nf) + | None -> assert false in let varno = List.length var_names in let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in (* initial sanity check *) @@ -339,7 +337,7 @@ let solve p = else check p (auto p) ;; -let run x y = solve (problem_of x y);; +Problems.main (solve ++ problem_of); (* Example usage of interactive: *) @@ -370,37 +368,3 @@ let run x y = solve (problem_of x y);; (* interactive "x y" "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat] ;; *) - -run "x x" ["x y"; "y y"; "y x"] ;; -run "x y" ["x (_. x)"; "y z"; "y x"] ;; -run "a (x. x b) (x. x c)" ["a (x. b b) @"; "a @ c"; "a (x. x x) a"; "a (a a a) (a c c)"] ;; - -run "x (y. x y y)" ["x (y. x y x)"] ;; - -run "x a a a a" [ - "x b a a a"; - "x a b a a"; - "x a a b a"; - "x a a a b"; -] ;; - -(* Controesempio ad usare un conto dei lambda che non considere le permutazioni *) -run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [ - "x a a a a (_. a) b b b"; - "x a a a a (_. _. _. _. x. y. x y)"; -] ;; - -(* bug in eat that was erasing terms in convergent that then diverged *) -run "x y z" -[ -"x @ @"; -"z (y @ (y @))" -] ;; - -(* bug in no_leading_lambdas where x in j-th position *) -run "v0 (v1 v2) (x. y. v0 v3 v4 v2)" -["v5 (v6 (x. v6) v7 v8 (x. v9) (x. v9 (v10 v10))) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y))) (v9 (x. v11) (v4 v8) (x. y. z. v12) (v4 v6 (x. v7 v11) v12) (x. x v8)) (v0 v3 v4 v9 (v7 v11) (v0 v3 v4 v2) v10) (v6 (x. v6) v7 v8 (v9 (x. v11) (v4 v8) (x. y. z. v12)) (v13 (x. y. y)) (v9 (x. v11) (v4 v8)))"] -;; - -print_hline(); -print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<" diff --git a/ocaml/simple.mli b/ocaml/simple.mli index 216e381..bdc6328 100644 --- a/ocaml/simple.mli +++ b/ocaml/simple.mli @@ -1,4 +1,5 @@ -(* type problem -val problem_of : string -> string list -> problem -val solve : problem -> unit *) -val run : string -> string list -> unit +type problem +val solve : problem -> unit +val problem_of : + string * Num.i_var option * Num.i_n_var list * Num.i_n_var list * + string list -> problem diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml index 8bdefdc..438b7b5 100644 --- a/ocaml/simple_test.ml +++ b/ocaml/simple_test.ml @@ -45,7 +45,10 @@ let main = repeat (fun _ -> let div, convs = gen complex vars in - Simple.run div convs + let str = "$ random simple test \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in + print_endline str; + let open Simple in + (solve ++ problem_of ++ Parser.problem_of_string) str ) num ; prerr_endline "\n---- ALL TESTS COMPLETED ----" -- 2.39.2