OCAMLC = ocamlopt -g -rectypes
LIB = unix.cmxa str.cmxa
-UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx
+UTILS = util.cmx console.cmx listx.cmx pure.cmx num.cmx parser.cmx parser_andrea.cmx
-all: a.out test4.out
+all: a.out test4.out andrea.out
run: test4.out
bash run
test4.out: $(UTILS) lambda4.cmx test.ml
$(OCAMLC) -o test4.out $(LIB) $^
+andrea.out: $(UTILS) andrea.ml
+ $(OCAMLC) -o andrea.out $(LIB) $(UTILS) andrea.ml
+
%.cmi: %.mli
$(OCAMLC) -c $<
--- /dev/null
+let (++) f g x = f (g x);;\r
+let id x = 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
+let eta_eq =\r
+ let rec aux l1 l2 t1 t2 = match t1, t2 with\r
+ | L t1, L t2 -> aux l1 l2 t1 t2\r
+ | L t1, t2 -> aux l1 (l2+1) t1 t2\r
+ | t1, L t2 -> aux (l1+1) l2 t1 t2\r
+ | V a, V b -> a + l1 = b + l2\r
+ | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2\r
+ | _, _ -> false\r
+ in aux 0 0\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
+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 =\r
+ function\r
+ | A(t,_) -> is_inert 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
+\r
+let rec head_of_inert = function\r
+ | V n -> n\r
+ | A(t, _) -> head_of_inert t\r
+ | _ -> assert false\r
+;;\r
+\r
+let rec args_no = function\r
+ | V _ -> 0\r
+ | A(t, _) -> 1 + args_no t\r
+ | _ -> assert false\r
+;;\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 " ^ 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 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 head_of_inert t1 = hd_var && n_args <= 1 + args_no 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 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
+let sanity p =\r
+ print_endline (string_of_problem p); (* non cancellare *)\r
+ if p.div = B then raise (Done p.sigma);\r
+ if not (is_inert p.div) then problem_fail p "p.div converged";\r
+ if p.conv = B then problem_fail p "p.conv diverged";\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
+(* eat the arguments of the divergent and explode.\r
+ It does NOT perform any check, may fail if done unsafely *)\r
+let eat p =\r
+print_cmd "EAT" "";\r
+ let var = head_of_inert p.div in\r
+ let n = args_no 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
+(* step on the head of div, on the k-th argument, with n fresh vars *)\r
+let step k n p =\r
+ let var = head_of_inert 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 (k-m)) 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_andrea.Lam t -> L (aux (level + 1) t)\r
+ | Parser_andrea.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_andrea.Var v -> V v\r
+ in let (tms, free) = Parser_andrea.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 inert_cut_at 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_eta_difference p t n_args =\r
+ let t = inert_cut_at n_args t in\r
+ let rec aux t u k = match t, u 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 (print_endline((string_of_t p t2) ^ " <> " ^ (string_of_t p u2)); k)\r
+ else aux t1 u1 (k-1)\r
+ | _, _ -> assert false\r
+ in aux p.div t n_args\r
+;;\r
+\r
+let rec no_leading_lambdas = function\r
+ | L t -> 1 + no_leading_lambdas t\r
+ | _ -> 0\r
+;;\r
+\r
+let compute_max_lambdas_at hd_var j =\r
+ let rec aux hd = function\r
+ | A(t1,t2) ->\r
+ (if head_of_inert t1 = hd && args_no t1 = j\r
+ then max (\r
+ if is_inert t2 && head_of_inert t2 = hd\r
+ then j - args_no t2\r
+ else no_leading_lambdas t2)\r
+ else id) (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 = head_of_inert p.div in\r
+ let n_args = args_no 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_eta_difference p t n_args - 1 in\r
+ let k = max\r
+ (compute_max_lambdas_at hd_var j p.div)\r
+ (compute_max_lambdas_at hd_var j 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 rec conv_join = function\r
+ | [] -> "@"\r
+ | x::xs -> conv_join xs ^ " ("^ x ^")"\r
+;;\r
+\r
+let _ = exec\r
+ "x x"\r
+ (conv_join["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
+auto (problem_of "x (y. x y y)" "x (y. x y x)");;\r
+\r
+auto (problem_of "x a a a a" (conv_join[\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
+auto (problem_of "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" (conv_join[\r
+ "x a a a a (_. a) b b b";\r
+ "x a a a a (_. _. _. _. x. y. x y)";\r
+]));\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
--- /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
--- /dev/null
+type term =\r
+ | Var of int\r
+ | App of term * term\r
+ | Lam of term\r
+\r
+exception ParsingError of string\r
+\r
+(* val problem_of_string:\r
+ string ->\r
+ string (* problem label *)\r
+ * Num.i_var option (* div *)\r
+ * Num.i_n_var list (* conv *)\r
+ * Num.i_n_var list (* ps *)\r
+ * string list (* names of free variables *)\r
+val from_file : string ->\r
+ (string (* problem label *)\r
+ * Num.i_var option (* div *)\r
+ * Num.i_n_var list (* conv *)\r
+ * Num.i_n_var list (* ps *)\r
+ * string list (* names of free variables *)) list *)\r
+\r
+ (* parses a string to a term *)\r
+ val parse: string -> term\r
+ (* parse many strings/terms, and returns the list of parsed terms + the list of free variables; variable 0 is not used *)\r
+ val parse_many: string list -> term list * string list\r
projects / fireball-separation.git / commitdiff