--- /dev/null
+let (++) f g x = f (g x);;\r
+\r
+let print_hline = Console.print_hline;;\r
+\r
+type var = int;;\r
+type t =\r
+ | V of var\r
+ | A of t * t\r
+ | L of t\r
+ | B (* bottom *)\r
+ | P (* pacman *)\r
+;;\r
+\r
+type problem = {\r
+ orig_freshno: int\r
+ ; freshno : int\r
+ ; div : t\r
+ ; conv : t\r
+ ; sigma : (var * t) list (* substitutions *)\r
+ ; stepped : var list\r
+}\r
+\r
+let all_terms p = [p.div; p.conv];;\r
+\r
+exception Done of (var * t) list (* substitution *);;\r
+exception Fail of int * string;;\r
+\r
+let string_of_t p =\r
+ let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
+ let rec string_of_term_w_pars level = function\r
+ | V v -> if v >= level then "`" ^ string_of_int (v-level) else\r
+ let nn = level - v-1 in\r
+ if nn < 5 then List.nth bound_vars nn else "x" ^ (string_of_int (nn-4))\r
+ | A _\r
+ | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"\r
+ | B -> "BOT"\r
+ | P -> "PAC"\r
+ and string_of_term_no_pars_app level = function\r
+ | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)\r
+ | _ as t -> string_of_term_w_pars level t\r
+ and string_of_term_no_pars_lam level = function\r
+ | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)\r
+ | _ as t -> string_of_term_no_pars level t\r
+ and string_of_term_no_pars level = function\r
+ | L _ as t -> string_of_term_no_pars_lam level t\r
+ | _ as t -> string_of_term_no_pars_app level t\r
+ in string_of_term_no_pars 0\r
+;;\r
+\r
+let string_of_problem p =\r
+ let lines = [\r
+ "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);\r
+ "[DV] " ^ (string_of_t p p.div);\r
+ "[CV] " ^ (string_of_t p p.conv);\r
+ ] in\r
+ String.concat "\n" lines\r
+;;\r
+\r
+let problem_fail p reason =\r
+ print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
+ print_endline (string_of_problem p);\r
+ raise (Fail (-1, reason))\r
+;;\r
+\r
+let freshvar ({freshno} as p) =\r
+ {p with freshno=freshno+1}, freshno+1\r
+;;\r
+\r
+let rec is_inert p =\r
+ function\r
+ | A(t,_) -> is_inert p t\r
+ | V _ -> true\r
+ | L _ | B | P -> false\r
+;;\r
+\r
+let is_var = function V _ -> true | _ -> false;;\r
+let is_lambda = function L _ -> true | _ -> false;;\r
+let is_pacman = function P -> true | _ -> false;;\r
+\r
+let rec subst level delift fromdiv sub =\r
+ function\r
+ | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
+ | L t -> L (subst (level + 1) delift fromdiv sub t)\r
+ | A (t1,t2) ->\r
+ let t1 = subst level delift fromdiv sub t1 in\r
+ let t2 = subst level delift fromdiv sub t2 in\r
+ if t1 = B || t2 = B then B else mk_app fromdiv t1 t2\r
+ | B -> B\r
+ | P -> P\r
+and mk_app fromdiv t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
+ | B | _ when t2 = B -> B\r
+ | L t1 -> subst 0 true fromdiv (0, t2) t1\r
+ | t1 -> A (t1, t2)\r
+and lift n =\r
+ let rec aux n' =\r
+ function\r
+ | V m -> V (if m >= n' then m + n else m)\r
+ | L t -> L (aux (n'+1) t)\r
+ | A (t1, t2) -> A (aux n' t1, aux n' t2)\r
+ | B -> B\r
+ | P -> P\r
+ in aux 0\r
+;;\r
+let subst = subst 0 false;;\r
+\r
+let subst_in_problem (sub: var * t) (p: problem) =\r
+print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
+ let p = {p with stepped=(fst sub)::p.stepped} in\r
+ let conv = subst false sub p.conv in\r
+ let div = subst true sub p.div in\r
+ let p = {p with div; conv} in\r
+ (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
+ {p with sigma=sub::p.sigma}\r
+;;\r
+\r
+let free_vars p t =\r
+ let rec aux level = function\r
+ | V v -> if v >= level then [v] else []\r
+ | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
+ | L t -> aux (level+1) t\r
+ | B | P -> []\r
+ in Util.sort_uniq (aux 0 t)\r
+;;\r
+\r
+let visible_vars p t =\r
+ let rec aux = function\r
+ | V v -> [v]\r
+ | A(t1,t2) -> (aux t1) @ (aux t2)\r
+ | B | P\r
+ | L _ -> []\r
+ (* | Ptr n -> aux (get_conv p n) *)\r
+ in Util.sort_uniq (aux t)\r
+;;\r
+\r
+let rec hd_of = function\r
+ | V n -> n\r
+ | A(t, _) -> hd_of t\r
+ | _ -> assert false\r
+;;\r
+\r
+let rec nargs = function\r
+ | V _ -> 0\r
+ | A(t, _) -> 1 + nargs t\r
+ | _ -> assert false\r
+;;\r
+\r
+let get_subterm_with_head_and_args hd_var n_args =\r
+ let rec aux = function\r
+ | V _ | L _ | B | P -> None\r
+ | A(t1,t2) as t ->\r
+ if hd_of t1 = hd_var && n_args <= 1 + nargs t1\r
+ then Some t\r
+ else match aux t2 with\r
+ | None -> aux t1\r
+ | Some _ as res -> res\r
+ in aux\r
+;;\r
+\r
+let rec eta_eq l1 l2 t1 t2 = match t1, t2 with\r
+ | L t1, L t2 -> eta_eq l1 l2 t1 t2\r
+ | L t1, t2 -> eta_eq l1 (l2+1) t1 t2\r
+ | t1, L t2 -> eta_eq (l1+1) l2 t1 t2\r
+ | V a, V b -> a + l1 = b + l2\r
+ | A(t1,t2), A(u1,u2) -> eta_eq l1 l2 t1 u1 && eta_eq l1 l2 t2 u2\r
+ | _, _ -> false\r
+;;\r
+let eta_eq = eta_eq 0 0;;\r
+\r
+\r
+let rec simple_explode p =\r
+ match p.div with\r
+ | V var ->\r
+ let subst = var, B in\r
+ sanity (subst_in_problem subst p)\r
+ | _ -> p\r
+\r
+and sanity p =\r
+ (* Sanity checks: *)\r
+ if (function | P | L _ -> true | _ -> false) p.div then problem_fail p "p.div converged";\r
+ if p.conv = B then problem_fail p "p.conv diverged";\r
+\r
+ print_endline (string_of_problem p); (* non cancellare *)\r
+ if p.div = B then raise (Done p.sigma);\r
+ let p = if is_var p.div then simple_explode p else p in\r
+ p\r
+;;\r
+\r
+let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
+\r
+let eat p =\r
+print_cmd "EAT" "";\r
+ let var = hd_of p.div in\r
+ let n = nargs p.div in\r
+ let rec aux m t =\r
+ if m = 0\r
+ then lift n t\r
+ else L (aux (m-1) t) in\r
+ let subst = var, aux n B in\r
+ sanity (subst_in_problem subst p)\r
+;;\r
+\r
+let step k n p =\r
+ let var = hd_of p.div in\r
+ print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
+ let rec aux' p m t =\r
+ if m < 0\r
+ then p, t\r
+ else\r
+ let p, v = freshvar p in\r
+ let p, t = aux' p (m-1) t in\r
+ p, A(t, V (v + k + 1)) in\r
+ let p, t = aux' p n (V 0) in\r
+ let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (m+1)) in\r
+ let rec aux m t =\r
+ if m < 0\r
+ then aux' (k-1) t\r
+ else L (aux (m-1) t) in\r
+ let t = aux k t in\r
+ let subst = var, t in\r
+ sanity (subst_in_problem subst p)\r
+;;\r
+\r
+let parse strs =\r
+ let rec aux level = function\r
+ | Parser.Lam t -> L (aux (level + 1) t)\r
+ | Parser.App (t1, t2) ->\r
+ if level = 0 then mk_app false (aux level t1) (aux level t2)\r
+ else A(aux level t1, aux level t2)\r
+ | Parser.Var v -> V v\r
+ in let (tms, free) = Parser.parse_many strs\r
+ in (List.map (aux 0) tms, free)\r
+;;\r
+\r
+let problem_of div conv =\r
+ print_hline ();\r
+ let all_tms, var_names = parse ([div; conv]) in\r
+ let div, conv = List.hd all_tms, List.hd (List.tl all_tms) in\r
+ let varno = List.length var_names in\r
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]} in\r
+ (* activate bombs *)\r
+ let p = try\r
+ let subst = Util.index_of "BOMB" var_names, L B in\r
+ subst_in_problem subst p\r
+ with Not_found -> p in\r
+ (* activate pacmans *)\r
+ let p = try\r
+ let subst = Util.index_of "PACMAN" var_names, P in\r
+ let p = subst_in_problem subst p in\r
+ (print_endline ("after subst in problem " ^ string_of_problem p); p)\r
+ with Not_found -> p in\r
+ (* initial sanity check *)\r
+ sanity p\r
+;;\r
+\r
+let exec div conv cmds =\r
+ let p = problem_of div conv in\r
+ try\r
+ problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
+ with\r
+ | Done _ -> ()\r
+;;\r
+\r
+let cut_app n t =\r
+ let rec aux t =\r
+ match t with\r
+ | V _ as t -> 0, t\r
+ | A(t1,_) as t ->\r
+ let k', t' = aux t1 in\r
+ if k' = n then n, t'\r
+ else k'+1, t\r
+ | _ -> assert false\r
+ in snd (aux t)\r
+;;\r
+\r
+let find_difference div conv n_args =\r
+ let conv = cut_app n_args conv in\r
+ let rec aux t1 t2 k = match t1, t2 with\r
+ | V _, V _ -> assert false (* div subterm of conv *)\r
+ | A(t1,t2), A(u1,u2) ->\r
+ if not (eta_eq t2 u2) then k\r
+ else aux t1 u1 (k-1)\r
+ | _, _ -> assert false\r
+ in aux div conv n_args\r
+;;\r
+\r
+let rec count_lams = function\r
+ | L t -> 1 + count_lams t\r
+ | _ -> 0\r
+;;\r
+\r
+let compute_k_from_args hd_var n_args =\r
+ let rec aux hd = function\r
+ | A(t1,t2) -> max (\r
+ if hd_of t1 = hd && (nargs t1) = (n_args - 1) then count_lams t2 else 0)\r
+ (max (aux hd t1) (aux hd t2))\r
+ | L t -> aux (hd+1) t\r
+ | V _ -> 0\r
+ | _ -> assert false\r
+ in aux hd_var\r
+;;\r
+\r
+let rec auto p =\r
+ let hd_var = hd_of p.div in\r
+ let n_args = nargs p.div in\r
+ match get_subterm_with_head_and_args hd_var n_args p.conv with\r
+ | None ->\r
+ (try let p = eat p in problem_fail p "Auto did not complete the problem" with Done _ -> ())\r
+ | Some t ->\r
+ let j = find_difference p.div p.conv n_args - 1 in\r
+ let k = max\r
+ (compute_k_from_args hd_var n_args p.div)\r
+ (compute_k_from_args hd_var n_args p.conv) in\r
+ let p = step j k p in\r
+ auto p\r
+;;\r
+\r
+let interactive div conv cmds =\r
+ let p = problem_of div conv in\r
+ try (\r
+ let p = List.fold_left (|>) p cmds in\r
+ let rec f p cmds =\r
+ let nth spl n = int_of_string (List.nth spl n) in\r
+ let read_cmd () =\r
+ let s = read_line () in\r
+ let spl = Str.split (Str.regexp " +") s in\r
+ s, let uno = List.hd spl in\r
+ try if uno = "eat" then eat\r
+ else if uno = "step" then step (nth spl 1) (nth spl 2)\r
+ else failwith "Wrong input."\r
+ with Failure s -> print_endline s; (fun x -> x) in\r
+ let str, cmd = read_cmd () in\r
+ let cmds = (" " ^ str ^ ";")::cmds in\r
+ try\r
+ let p = cmd p in f p cmds\r
+ with\r
+ | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
+ in f p []\r
+ ) with Done _ -> ()\r
+;;\r
+\r
+let _ = exec\r
+ "x x"\r
+ "@ (x y) (y y) (y x)"\r
+ [ step 0 0; eat ]\r
+;;\r
+\r
+auto (problem_of "x x" "@ (x y) (y y) (y x)");;\r
+auto (problem_of "x y" "@ (x (_. x)) (y z) (y x)");;\r
+auto (problem_of "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))");;\r
+\r
+interactive "x y"\r
+"@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat] ;;\r
+\r
+(* let _ = exec\r
+ "x y"\r
+ [ "x x"; "y z"; "y x" ]\r
+ [ step 0 0 0; step 1 0 1; eat 5; ]\r
+;;\r
+\r
+let _ = exec\r
+ "a b c"\r
+ [ "a b @"; "a @ c"; "a a a" ]\r
+ [ step 0 0 0; step 1 1 0; eat 2; ]\r
+;;\r
+\r
+let _ = exec\r
+ "a (a b c) (a d e)"\r
+ [ "a (a b @) (a @ e)"; "a a a" ]\r
+ [ step 0 0 0; step 1 1 0; eat 2]\r
+;; *)\r
+\r
+print_hline();\r
+print_endline "ALL DONE. "\r
+\r
+(* TEMPORARY TESTING FACILITY BELOW HERE *)\r
+\r
+let acaso l =\r
+ let n = Random.int (List.length l) in\r
+ List.nth l n\r
+;;\r
+\r
+let acaso2 l1 l2 =\r
+ let n1 = List.length l1 in\r
+ let n = Random.int (n1 + List.length l2) in\r
+ if n >= n1 then List.nth l2 (n - n1) else List.nth l1 n\r
+;;\r
+\r
+let gen n vars =\r
+ let rec aux n inerts lams =\r
+ if n = 0 then List.hd inerts, List.hd (Util.sort_uniq (List.tl inerts))\r
+ else let inerts, lams = if Random.int 2 = 0\r
+ then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams\r
+ else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams\r
+ in aux (n-1) inerts lams\r
+ in aux (2*n) vars []\r
+;;\r
+\r
+let f () =\r
+ let complex = 200 in\r
+ let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in\r
+ gen complex vars\r
+\r
+ let rec repeat f n =\r
+ prerr_endline "\n########################### NEW TEST ###########################";\r
+ f () ;\r
+ if n > 0 then repeat f (n-1)\r
+ ;;\r
+\r
+\r
+let main () =\r
+ Random.self_init ();\r
+ repeat (fun _ ->\r
+ let div, conv = f () in\r
+ auto (problem_of div conv)\r
+ ) 100;\r
+;;\r
+\r
+(* main ();; *)\r
projects / fireball-separation.git / commitdiff