+++ /dev/null
-type term =\r
- | Var of int\r
- | App of term * term\r
- | Lam of term\r
-;;\r
-\r
-let mk_app x y = App(x, y);;\r
-let mk_lam x = Lam x;;\r
-let mk_var x = Var x;;\r
-\r
-exception ParsingError of string;;\r
-\r
-let isAlphaNum c = let n = Char.code c in\r
- (48 <= n && n <= 90) || (95 <= n && n <= 122) ;;\r
-let isSpace c = c = ' ' || c = '\n' || c = '\t' ;;\r
-\r
-(* FIXME *)\r
-let mk_var' (bound, free) x =\r
- if x <> "@" && List.mem x bound\r
- then free, mk_var (Util.index_of x bound)\r
- else if x <> "@" && List.mem x free\r
- then free, mk_var (List.length bound + Util.index_of x free)\r
- else (free @ [x]), mk_var (List.length bound + List.length free)\r
-;;\r
-\r
-let mk_app' = function\r
- | [] -> assert false\r
- | t :: ts -> List.fold_left mk_app t ts\r
-;;\r
-\r
-let explode s =\r
- let len = String.length s in\r
- let rec aux i l =\r
- if i >= len || s.[i] = '#' then l else aux (i+1) (s.[i] :: l)\r
- in List.rev (aux 0 [])\r
-;;\r
-\r
-let implode l =\r
- let res = String.create (List.length l) in\r
- let rec aux i = function\r
- | [] -> res\r
- | c :: l -> String.set res i c; aux (i + 1) l in\r
- aux 0 l\r
-;;\r
-\r
-let rec strip_spaces = function\r
- | c::cs when isSpace c -> strip_spaces cs\r
- | cs -> cs\r
-;;\r
-\r
-let read_var s =\r
- let rec aux = function\r
- | [] -> None, []\r
- | c::cs as x ->\r
- if c = '@' then\r
- (if cs <> [] && (let hd = List.hd cs in hd = '@' || isAlphaNum hd)\r
- then raise (ParsingError ("Unexpected `"^String.make 1 (List.hd cs)^"` after `@`."))\r
- else Some['@'], cs)\r
- else if isAlphaNum c\r
- then match aux cs with\r
- | (Some x), cs' -> Some (c :: x), cs'\r
- | None, cs' -> (Some [c]), cs'\r
- else None, x\r
- in match aux s with\r
- | None, y -> None, y\r
- | Some x, y -> Some (implode x), y\r
-;;\r
-\r
-let read_var' (bound, free as vars) s =\r
- match read_var s with\r
- | Some varname, cs ->\r
- let free, v = mk_var' vars varname in\r
- Some [v], cs, (bound, free)\r
- | None, _ -> raise (ParsingError ("Can't read variable"))\r
-;;\r
-\r
-let rec read_smt vars =\r
- let check_if_lambda cs = match read_var cs with\r
- | None, _ -> false\r
- | Some x, cs -> match strip_spaces cs with\r
- | [] -> false\r
- | c::_ -> c = '.'\r
- in let read_lambda (bound, free) cs = (\r
- match read_var (strip_spaces cs) with\r
- | Some varname, cs ->\r
- let vars' = (varname::bound, free) in\r
- (match strip_spaces cs with\r
- | [] -> raise (ParsingError "Lambda expression incomplete")\r
- | c::cs -> (if c = '.' then (match read_smt vars' cs with\r
- | None, _, _ -> raise (ParsingError "Lambda body expected")\r
- | Some [x], y, (_, free) -> Some [mk_lam x], y, (bound, free)\r
- | Some _, _, _ -> assert false\r
- ) else raise (ParsingError "Expected `.` after variable in lambda")\r
- ))\r
- | _, _ -> assert false\r
- ) in let rec aux vars cs =\r
- match strip_spaces cs with\r
- | [] -> None, [], vars\r
- | c::_ as x ->\r
- let tms, cs, vars = (\r
- if c = '(' then read_pars vars x\r
- else if c = ')' then (None, x, vars)\r
- else if check_if_lambda x then read_lambda vars x\r
- else read_var' vars x) in\r
- match tms with\r
- | Some [tm] -> (\r
- match aux vars cs with\r
- | None, cs, vars -> Some [tm], cs, vars\r
- | Some ts, cs, vars -> Some (tm :: ts), cs, vars\r
- )\r
- | Some _ -> assert false\r
- | None -> None, x, vars\r
- in fun cs -> match aux vars cs with\r
- | None, cs, vars -> None, cs, vars\r
- | Some ts, cs, vars -> Some [mk_app' ts], cs, vars\r
-and read_pars vars = function\r
- | [] -> None, [], vars\r
- | c::cs -> if c = '(' then (\r
- let tm, cs, vars = read_smt vars cs in\r
- let cs = strip_spaces cs in\r
- match cs with\r
- | [] -> None, [], vars\r
- | c::cs -> if c = ')' then tm, cs, vars else raise (ParsingError "Missing `)`")\r
- ) else assert false\r
-;;\r
-\r
-let parse x =\r
- match read_smt ([],[]) (explode x) with\r
- | Some [y], [], _ -> y\r
- | _, _, _ -> assert false\r
-;;\r
-\r
-let parse_many strs =\r
- let f (x, y) z = match read_smt y (explode z) with\r
- | Some[tm], [], vars -> (tm :: x, vars)\r
- | _, _, _ -> assert false\r
- in let aux = List.fold_left f ([], ([], []))\r
- in let (tms, (_, free)) = aux strs\r
- in (List.rev tms, free)\r
-;;\r
-\r
-(**********************************************************************\r
-\r
-let rec string_of_term = function\r
- | Tvar n -> string_of_int n\r
- | Tapp(t1, t2) -> "(" ^ string_of_term t1 ^ " " ^ string_of_term t2 ^ ")"\r
- | Tlam(t1) -> "(\\" ^ string_of_term t1 ^ ")"\r
-;;\r
-\r
-let _ = prerr_endline (">>>" ^ string_of_term (parse "(\\x. x y z z1 k) z1 z j"));;\r
-\r
-\r
-*******************************************************************************)\r
-\r
-(* let problem_of_string s =\r
- let lines = Str.split (Str.regexp "[\n\r\x0c\t;]+") s in\r
- let head, lines = List.hd lines, List.tl lines in\r
- let name = String.trim (String.sub head 1 (String.length head - 1)) in\r
- let lines = List.filter ((<>) "") lines in\r
- let aux (last, div, conv, ps) line =\r
- let chr = String.sub line 0 1 in\r
- let line = String.trim (String.sub line 1 (String.length line - 1)) in\r
- if line = "" then chr, div, conv, ps else\r
- let rec aux' chr line =\r
- if chr = "#"\r
- then chr, div, conv, ps\r
- else if chr = "D"\r
- then chr, line, conv, ps\r
- else if chr = "C"\r
- then chr, div, line::conv, ps\r
- else if chr = "N"\r
- then chr, div, conv, line::ps\r
- else if chr = " "\r
- then aux' last line\r
- else raise (ParsingError\r
- ("Unexpected at beginning of problem: `" ^ chr ^ "` " ^ line)) in\r
- aux' chr line in\r
- let _, div, conv, ps = List.fold_left aux ("#", "", [], []) lines in\r
- let div_provided = div <> "" in\r
- let div = if div_provided then div else "BOT" in\r
- let strs = [div] @ ps @ conv in\r
-\r
- if List.length ps = 0 && List.length conv = 0\r
- then raise (ParsingError "Parsed empty problem");\r
-\r
- (* parse' *)\r
- let (tms, free) = parse_many strs in\r
- (* Replace pacmans and bottoms *)\r
- let n_bot = try Util.index_of "BOT" free with Not_found -> min_int in\r
- let n_pac = try Util.index_of "PAC" free with Not_found -> min_int in\r
- let n_bomb = try Util.index_of "BOMB" free with Not_found -> min_int in\r
- let fix lev v =\r
- if v = lev + n_bot then `Bottom\r
- else if v = lev + n_pac then `Pacman\r
- else if v = lev + n_bomb then `Lam(true, `Bottom)\r
- else if v = lev then `Var(v, min_int) (* zero *)\r
- else `Var(v,1) in (* 1 by default when variable not applied *)\r
- (* Fix arity *)\r
- let open Num in\r
- let exclude_bottom = function\r
- | #nf_nob as t -> t\r
- (* actually, the following may be assert false *)\r
- | `Bottom -> raise (ParsingError "Input term not in normal form") in\r
- let rec aux_nob lev : nf_nob -> nf = function\r
- | `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)\r
- | `Var(n,_) -> fix lev n\r
- | `Lam(_,t) -> `Lam (true, aux (lev+1) t)\r
- | `Match _ | `N _ -> assert false\r
- | `Pacman -> `Pacman\r
- and aux lev : Num.nf -> Num.nf = function\r
- | #nf_nob as t -> aux_nob lev t\r
- | `Bottom -> assert false in\r
-let all_tms = List.map (aux 0) (tms :> Num.nf list) in\r
-\r
-(* problem_of *)\r
-let div, (ps, conv) = List.hd all_tms, Util.list_cut (List.length ps, List.tl all_tms) in\r
-\r
-let div = if not div_provided || div = `Bottom\r
- then None\r
- else match div with\r
- | `I _ as t -> Some t\r
- | _ -> raise (ParsingError "D is not an inert in the initial problem") in\r
-let conv = Util.filter_map (\r
- function\r
- | #i_n_var as t -> Some t\r
- | `Lam _ -> None\r
- | _ -> raise (ParsingError "A C-term is not i_n_var")\r
- ) conv in\r
-let ps = List.map (\r
- function\r
- | #i_n_var as y -> y\r
- | _ -> raise (ParsingError "An N-term is not i_n_var")\r
- ) ps in\r
- name, div, conv, ps, free\r
-;;\r
-\r
-\r
-let from_file path =\r
- let lines = ref ["#"] in\r
- let chan = open_in path in\r
- let _ = try\r
- while true; do\r
- lines := input_line chan :: !lines\r
- done\r
- with End_of_file ->\r
- close_in chan in\r
- let txt = String.concat "\n" (List.rev !lines) in\r
- let problems = Str.split (Str.regexp "[\n\r]+\\$") txt in\r
- List.map problem_of_string (List.tl (List.map ((^) "$") problems))\r
-;; *)\r
-\r
-let parse x =\r
- match read_smt ([],[]) (explode x) with\r
- | Some [y], [], _ -> y\r
- | _, _, _ -> assert false\r
-;;\r
-\r
-\r
-let parse_many strs =\r
- let f (x, y) z = match read_smt y (explode z) with\r
- | Some[tm], [], vars -> (tm :: x, vars)\r
- | _, _, _ -> assert false\r
- in let aux = List.fold_left f ([], ([], []))\r
- in let (tms, (_, free)) = aux strs\r
- in (List.rev tms, free)\r
-;;\r
let p = subst_in_problem subst p in\r
sanity p\r
;;\r
-;;\r
\r
-let parse strs =\r
- let rec aux level = function\r
- | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
- | Parser_andrea.App (t1, t2) ->\r
- if level = 0 then mk_app (aux level t1) (aux level t2)\r
- else A(aux level t1, aux level t2)\r
- | Parser_andrea.Var v -> V v in\r
- let (tms, free) = Parser_andrea.parse_many strs in\r
- (List.map (aux 0) tms, free)\r
;;\r
\r
+\r
let rec auto p =\r
let hd_var, n_args = get_inert p.div in\r
match get_subterm_with_head_and_args hd_var n_args p.conv with\r
auto p\r
;;\r
\r
-let problem_of div convs =\r
- let rec conv_join = function\r
- | [] -> "@"\r
- | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
+let problem_of (label, div, convs, ps, var_names) =\r
print_hline ();\r
- let conv = conv_join convs in\r
- let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
+ let rec aux = function\r
+ | `Lam(_, t) -> L (aux t)\r
+ | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app x (aux y)) (V v) args\r
+ | `Var(v,_) -> V v\r
+ | `N _ | `Match _ -> assert false in\r
+ assert (List.length ps = 0);\r
+ let convs = List.rev convs in\r
+ let conv = List.fold_left (fun x y -> mk_app x (aux (y :> Num.nf))) (V (List.length var_names)) convs in\r
+ let var_names = "@" :: var_names in\r
+ let div = match div with\r
+ | Some div -> aux (div :> Num.nf)\r
+ | None -> assert false in\r
let varno = List.length var_names in\r
let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
(* initial sanity check *)\r
else check p (auto p)\r
;;\r
\r
-let run x y = solve (problem_of x y);;\r
+Problems.main (solve ++ problem_of);\r
\r
(* Example usage of interactive: *)\r
\r
(* interactive "x y"\r
"@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
;; *)\r
-\r
-run "x x" ["x y"; "y y"; "y x"] ;;\r
-run "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
-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)"] ;;\r
-\r
-run "x (y. x y y)" ["x (y. x y x)"] ;;\r
-\r
-run "x a a a a" [\r
- "x b a a a";\r
- "x a b a a";\r
- "x a a b a";\r
- "x a a a b";\r
-] ;;\r
-\r
-(* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
-run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
- "x a a a a (_. a) b b b";\r
- "x a a a a (_. _. _. _. x. y. x y)";\r
-] ;;\r
-\r
-(* bug in eat that was erasing terms in convergent that then diverged *)\r
-run "x y z"\r
-[\r
-"x @ @";\r
-"z (y @ (y @))"\r
-] ;;\r
-\r
-(* bug in no_leading_lambdas where x in j-th position *)\r
-run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
-["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)))"]\r
-;;\r
-\r
-print_hline();\r
-print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r