type t =\r
| V of var\r
| A of t * t\r
- | L of t\r
- | B (* bottom *)\r
- | C of int\r
+ | L of (t * t list (*garbage*))\r
+ | C (* constant *)\r
;;\r
\r
-let delta = L(A(V 0, V 0));;\r
+let delta = L(A(V 0, V 0),[]);;\r
+\r
+let rec is_stuck = function\r
+ | C -> true\r
+ | A(t,_) -> is_stuck t\r
+ | _ -> false\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
+ let rec aux l1 l2 t1 t2 =\r
+ let stuck1, stuck2 = is_stuck t1, is_stuck t2 in\r
+ match t1, t2 with\r
+ | _, _ when not stuck1 && stuck2 -> false\r
+ | _, _ when stuck1 -> true\r
+ | L t1, L t2 -> aux l1 l2 (fst t1) (fst t2)\r
+ | L t1, t2 -> aux l1 (l2+1) (fst t1) t2\r
+ | t1, L t2 -> aux (l1+1) l2 t1 (fst t2)\r
| V a, V b -> a + l1 = b + l2\r
- | C a, C b -> a = b\r
| A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2\r
| _, _ -> false\r
in aux ;;\r
\r
(* is arg1 eta-subterm of arg2 ? *)\r
let eta_subterm u =\r
- let rec aux lev t = eta_eq' lev 0 u t || match t with\r
- | L t -> aux (lev+1) t\r
+ let rec aux lev t = if t = C then false else (eta_eq' lev 0 u t || match t with\r
+ | L(t,g) -> List.exists (aux (lev+1)) (t::g)\r
| A(t1, t2) -> aux lev t1 || aux lev t2\r
- | _ -> false\r
- in aux 0\r
+ | _ -> false) in\r
+ aux 0\r
;;\r
\r
(* does NOT lift the argument *)\r
-let mk_lams = fold_nat (fun x _ -> L x) ;;\r
+let mk_lams = fold_nat (fun x _ -> L(x,[])) ;;\r
\r
let string_of_t =\r
let string_of_bvar =\r
let rec string_of_term_w_pars level = function\r
| V v -> if v >= level then "`" ^ string_of_int (v-level) else\r
string_of_bvar (level - v-1)\r
- | C n -> "c" ^ string_of_int n\r
+ | C -> "C"\r
| A _\r
| L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
- | B -> "BOT"\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 level = function\r
- | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r
+ | L(t,g) -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r
+ ^ (if g = [] then "" else String.concat ", " ("" :: List.map (string_of_term_w_pars (level+1)) g))\r
| _ as t -> string_of_term_no_pars_app level t\r
in string_of_term_no_pars 0\r
;;\r
type problem = {\r
orig_freshno: int\r
; freshno : int\r
+ ; label : string\r
; div : t\r
; conv : t\r
; sigma : (var * t) list (* substitutions *)\r
- ; stepped : var list\r
- ; phase : [`One | `Two] (* :'( *)\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.div;\r
"[CV] " ^ string_of_t p.conv;\r
] in\r
String.concat "\n" lines\r
;;\r
\r
+exception B;;\r
exception Done of (var * t) list (* substitution *);;\r
-exception Fail of int * string;;\r
+exception Unseparable of string;;\r
+exception Backtrack of string;;\r
+\r
+let rec try_all label f = function\r
+ | x::xs -> (try f x with Backtrack _ -> try_all label f xs)\r
+ | [] -> raise (Backtrack label)\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
+ failwith reason\r
;;\r
\r
let freshvar ({freshno} as p) =\r
{p with freshno=freshno+1}, freshno+1\r
;;\r
\r
+(* CSC: rename? is an applied C an inert?\r
+ is_inert and get_inert work inconsistently *)\r
let rec is_inert =\r
function\r
| A(t,_) -> is_inert t\r
| V _ -> true\r
- | C _\r
- | L _ | B -> false\r
+ | C\r
+ | L _ -> false\r
;;\r
\r
-let is_var = function V _ -> true | _ -> false;;\r
-let is_lambda = function L _ -> true | _ -> false;;\r
+let rec is_constant =\r
+ function\r
+ C -> true\r
+ | V _ -> false\r
+ | A(t,_)\r
+ | L(t,_) -> is_constant t\r
+;;\r
\r
let rec get_inert = function\r
- | V n -> (n,0)\r
+ | V _ | C as t -> (t,0)\r
| A(t, _) -> let hd,args = get_inert t in hd,args+1\r
| _ -> assert false\r
;;\r
\r
-let rec no_leading_lambdas hd_var j = function\r
- | L t -> 1 + no_leading_lambdas (hd_var+1) j t\r
- | A _ as t -> let hd_var', n = get_inert t in if hd_var = hd_var' then max 0 (j - n) else 0\r
- | V n -> if n = hd_var then j else 0\r
- | B | C _ -> 0\r
+let args_of_inert =\r
+ let rec aux acc =\r
+ function\r
+ | V _ | C -> acc\r
+ | A(t, a) -> aux (a::acc) t\r
+ | _ -> assert false\r
+ in\r
+ aux []\r
+;;\r
+\r
+(* precomputes the number of leading lambdas in a term,\r
+ after replacing _v_ w/ a term starting with n lambdas *)\r
+let rec no_leading_lambdas v n = function\r
+ | L(t,_) -> 1 + no_leading_lambdas (v+1) n t\r
+ | A _ as t -> let v', m = get_inert t in if V v = v' then max 0 (n - m) else 0\r
+ | V v' -> if v = v' then n else 0\r
+ | C -> 0\r
;;\r
+\r
let rec subst level delift 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 -> let t = subst (level + 1) delift sub t in if t = B then B else L t\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 x -> let t, g = subst_in_lam (level+1) delift sub x in L(t, g), []\r
| A (t1,t2) ->\r
- let t1 = subst level delift sub t1 in\r
- let t2 = subst level delift sub t2 in\r
- mk_app t1 t2\r
- | C _ as t -> t\r
- | B -> B\r
-and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
+ let t1, g1 = subst level delift sub t1 in\r
+ let t2, g2 = subst level delift sub t2 in\r
+ let t3, g3 = mk_app t1 t2 in\r
+ t3, g1 @ g2 @ g3\r
+ | C -> C, []\r
+and subst_in_lam level delift sub (t, g) =\r
+ let t', g' = subst level delift sub t in\r
+ let g'' = List.fold_left\r
+ (fun xs t ->\r
+ let x,y = subst level delift sub t in\r
+ (x :: y @ xs)) g' g in t', g''\r
+and mk_app t1 t2 = if t1 = delta && t2 = delta then raise B\r
else match t1 with\r
- | B -> B\r
- | L t1 -> subst 0 true (0, t2) t1\r
- | _ -> A (t1, t2)\r
+ | L x -> subst_in_lam 0 true (0, t2) x\r
+ | _ -> A (t1, t2), []\r
and lift n =\r
let rec aux lev =\r
function\r
| V m -> V (if m >= lev then m + n else m)\r
- | L t -> L (aux (lev+1) t)\r
+ | L(t,g) -> L (aux (lev+1) t, List.map (aux (lev+1)) g)\r
| A (t1, t2) -> A (aux lev t1, aux lev t2)\r
- | C _ as t -> t\r
- | B -> B\r
+ | C -> C\r
in aux 0\r
;;\r
-let subst = subst 0 false;;\r
-\r
-let subst_in_problem sub p =\r
-print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));\r
- {p with\r
- div=subst sub p.div;\r
- conv=subst sub p.conv;\r
- stepped=(fst sub)::p.stepped;\r
- sigma=sub::p.sigma}\r
+let subst' = subst;;\r
+let subst = subst' 0 false;;\r
+\r
+let rec mk_apps t = function\r
+ | u::us -> mk_apps (A(t,u)) us\r
+ | [] -> t\r
;;\r
\r
-let get_subterm_with_head_and_args hd_var n_args =\r
- let rec aux lev = function\r
- | C _\r
- | V _ | B -> None\r
- | L t -> aux (lev+1) t\r
+let subst_in_problem ((v, t) as sub) p =\r
+print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);\r
+ let sigma = sub :: p.sigma in\r
+ let div, g = try subst sub p.div with B -> raise (Done sigma) in\r
+ let divs = div :: g in\r
+ let conv, g = try subst sub p.conv with B -> raise (Backtrack "p.conv diverged") in\r
+ let conv = if g = [] then conv else mk_apps C (conv::g) in\r
+ divs, {p with div; conv; sigma}\r
+;;\r
+\r
+let get_subterms_with_head hd_var =\r
+ let rec aux lev inert_done g = function\r
+ | L(t,g') -> List.fold_left (aux (lev+1) false) g (t::g')\r
+ | C | V _ -> g\r
| A(t1,t2) as t ->\r
let hd_var', n_args' = get_inert t1 in\r
- if hd_var' = hd_var + lev && n_args <= 1 + n_args'\r
- then Some (lift ~-lev t)\r
- else match aux lev t2 with\r
- | None -> aux lev t1\r
- | Some _ as res -> res\r
- in aux 0\r
+ if not inert_done && hd_var' = V (hd_var + lev)\r
+ then lift ~-lev t :: aux lev false (aux lev true g t1) t2\r
+ else aux lev false (aux lev true g t1) t2\r
+ in aux 0 false []\r
;;\r
\r
-let rec purify = function\r
- | L t -> Pure.L (purify t)\r
- | A (t1,t2) -> Pure.A (purify t1, purify t2)\r
- | V n -> Pure.V n\r
- | C _ -> Pure.V max_int (* FIXME *)\r
- | B -> Pure.B\r
+let purify =\r
+ let rec aux = function\r
+ | L(t,g) ->\r
+ let t = aux (lift (List.length g) t) in\r
+ let t = List.fold_left (fun t g -> Pure.A(Pure.L t, aux g)) t g in\r
+ Pure.L t\r
+ | A (t1,t2) -> Pure.A (aux t1, aux t2)\r
+ | V n -> Pure.V (n)\r
+ | C -> Pure.V (min_int/2)\r
+ in aux\r
;;\r
\r
let check p sigma =\r
let div = purify p.div in\r
let conv = purify p.conv in\r
let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r
- let freshno = List.fold_right (fun (x,_) -> max x) sigma 0 in\r
+ let freshno = List.fold_right (max ++ fst) sigma 0 in\r
let env = Pure.env_of_sigma freshno sigma in\r
- assert (Pure.diverged (Pure.mwhd (env,div,[])));\r
- print_endline " D diverged.";\r
- assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));\r
- print_endline " C converged.";\r
+ (if not (Pure.diverged (Pure.mwhd (env,div,[])))\r
+ then failwith "D converged in Pure");\r
+ print_endline "- D diverged.";\r
+ (if Pure.diverged (Pure.mwhd (env,conv,[]))\r
+ then failwith "C diverged in Pure");\r
+ print_endline "- C converged.";\r
()\r
;;\r
\r
let sanity p =\r
print_endline (string_of_problem p); (* non cancellare *)\r
- if p.conv = B then problem_fail p "p.conv diverged";\r
- if p.div = B then raise (Done p.sigma);\r
- if p.phase = `Two && p.div = delta then raise (Done p.sigma);\r
- if not (is_inert p.div) then problem_fail p "p.div converged";\r
+ (* Trailing constant args can be removed because do not contribute to eta-diff *)\r
+ let rec remove_trailing_constant_args = function\r
+ | A(t1, t2) when is_constant t2 -> remove_trailing_constant_args t1\r
+ | _ as t -> t in\r
+ let p = {p with div=remove_trailing_constant_args p.div} in\r
p\r
;;\r
\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 t2) ^ " <> " ^ (string_of_t u2));*) k)\r
- else aux t1 u1 (k-1)\r
- | _, _ -> assert false\r
- in aux p.div t n_args\r
+(* return the index of the first argument with a difference\r
+ (the first argument is 0) *)\r
+let find_eta_difference p t =\r
+ let divargs = args_of_inert p.div in\r
+ let conargs = args_of_inert t in\r
+ let rec range i j =\r
+ if j = 0 then [] else i :: range (i+1) (j-1) in\r
+ let rec aux k divargs conargs =\r
+ match divargs,conargs with\r
+ [],conargs -> range k (List.length conargs)\r
+ | _::_,[] -> [k]\r
+ | t1::divargs,t2::conargs ->\r
+ (if not (eta_eq t1 t2) then [k] else []) @ aux (k+1) divargs conargs\r
+ in\r
+ aux 0 divargs conargs\r
;;\r
\r
let compute_max_lambdas_at hd_var j =\r
let rec aux hd = function\r
| A(t1,t2) ->\r
- (if get_inert t1 = (hd, j)\r
+ (if get_inert t1 = (V hd, j)\r
then max ( (*FIXME*)\r
- if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd\r
+ if is_inert t2 && let hd', j' = get_inert t2 in hd' = V hd\r
then let hd', j' = get_inert t2 in j - j'\r
else no_leading_lambdas hd_var j 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
+ | L(t,_) -> aux (hd+1) t\r
+ | V _ | C -> 0\r
in aux hd_var\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, k = get_inert p.div in\r
- let phase = p.phase in\r
- let p, t =\r
- match phase with\r
- | `One ->\r
- let n = 1 + max\r
- (compute_max_lambdas_at var k p.div)\r
- (compute_max_lambdas_at var k p.conv) in\r
- (* apply fresh vars *)\r
- let p, t = fold_nat (fun (p, t) _ ->\r
- let p, v = freshvar p in\r
- p, A(t, V (v + k))\r
- ) (p, V 0) n in\r
- let p = {p with phase=`Two} in p, A(t, delta)\r
- | `Two -> p, delta in\r
- let subst = var, mk_lams t k in\r
- let p = subst_in_problem subst p in\r
- sanity p;\r
- let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in\r
- sanity p\r
+(* returns Some i if i is the smallest integer s.t. p holds for the i-th\r
+ element of the list in input *)\r
+let smallest_such_that p =\r
+ let rec aux i =\r
+ function\r
+ [] -> None\r
+ | hd::_ when (print_endline (string_of_t hd) ; p hd) -> Some i\r
+ | _::tl -> aux (i+1) tl\r
+ in\r
+ aux 0\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, _ = get_inert p.div in\r
-print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
+ let hd, _ = get_inert p.div in\r
+ match hd with\r
+ | C | L _ | A _ -> assert false\r
+ | V var ->\r
+print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (on " ^ string_of_int (k+1) ^ "th)");\r
let p, t = (* apply fresh vars *)\r
fold_nat (fun (p, t) _ ->\r
let p, v = freshvar p in\r
fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
let t = mk_lams t (k+1) in (* make leading lambdas *)\r
let subst = var, t in\r
- let p = subst_in_problem subst p in\r
- sanity p\r
-;;\r
+ let divs, p = subst_in_problem subst p in\r
+ divs, sanity 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 (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
+let finish p =\r
+ (* one-step version of eat *)\r
+ let compute_max_arity =\r
+ let rec aux n = function\r
+ | A(t1,t2) -> max (aux (n+1) t1) (aux 0 t2)\r
+ | L(t,g) -> List.fold_right (max ++ (aux 0)) (t::g) 0\r
+ | _ -> n\r
+ in aux 0 in\r
+print_cmd "FINISH" "";\r
+ (* First, a step on the last argument of the divergent.\r
+ Because of the sanity check, it will never be a constant term. *)\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let div_hd = match div_hd with V n -> n | _ -> assert false in\r
+ let j = div_nargs - 1 in\r
+ let arity = compute_max_arity p.conv in\r
+ let n = 1 + arity + max\r
+ (compute_max_lambdas_at div_hd j p.div)\r
+ (compute_max_lambdas_at div_hd j p.conv) in\r
+ let _, p = step j n p in\r
+ (* Now, find first argument of div that is a variable never applied anywhere.\r
+ It must exist because of some invariant, since we just did a step,\r
+ and because of the arity of the divergent *)\r
+ let div_hd, div_nargs = get_inert p.div in\r
+ let div_hd = match div_hd with V n -> n | _ -> assert false in\r
+ let rec aux m = function\r
+ | A(t, V delta_var) ->\r
+ if delta_var <> div_hd && get_subterms_with_head delta_var p.conv = []\r
+ then m, delta_var\r
+ else aux (m-1) t\r
+ | A(t,_) -> aux (m-1) t\r
+ | _ -> assert false in\r
+ let m, delta_var = aux div_nargs p.div in\r
+ let _, p = subst_in_problem (delta_var, delta) p in\r
+ let _, p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in\r
+ sanity p\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
- | None ->\r
- (try\r
- let phase = p.phase in\r
- let p = eat p in\r
- if phase = `Two\r
- then problem_fail p "Auto.2 did not complete the problem"\r
- else auto p\r
- with Done sigma -> sigma)\r
- | Some t ->\r
- let j = find_eta_difference p t n_args - 1 in\r
- let k = 1 + 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
+let auto p =\r
+ let rec aux p =\r
+ match p.div with\r
+ | L(div,g) -> (* case p.div is an abstraction *)\r
+ let f l t = fst (subst' 0 true (0, C) t) :: l in\r
+ (* the `fst' above is because we can ignore the\r
+ garbage generated by the subst, because substituting\r
+ C does not create redexes and thus no new garbage is activated *)\r
+ let tms = List.fold_left f [] (div::g) in\r
+ try_all "auto.L"\r
+ (fun div -> aux {p with div}) tms\r
+ | _ -> (\r
+ if is_constant p.div (* case p.div is rigid inert *)\r
+ then try_all "auto.C"\r
+ (fun div -> aux {p with div}) (args_of_inert p.div)\r
+ else (* case p.div is flexible inert *)\r
+ let hd, n_args = get_inert p.div in\r
+ match hd with\r
+ | C | L _ | A _ -> assert false\r
+ | V hd_var ->\r
+ let tms = get_subterms_with_head hd_var p.conv in\r
+ if List.exists (fun t -> snd (get_inert t) >= n_args) tms\r
+ then (\r
+ (* let tms = List.sort (fun t1 t2 -> - compare (snd (get_inert t1)) (snd (get_inert t2))) tms in *)\r
+ try_all "no similar terms" (fun t ->\r
+ let js = find_eta_difference p t in\r
+ (* print_endline (String.concat ", " (List.map string_of_int js)); *)\r
+ let js = List.rev js in\r
+ try_all "no eta difference"\r
+ (fun j ->\r
+ let k = 1 + max\r
+ (compute_max_lambdas_at hd_var j p.div)\r
+ (compute_max_lambdas_at hd_var j p.conv) in\r
+ let divs, p = step j k p in\r
+ try_all "p.div" (fun div -> aux (sanity {p with div})) divs\r
+ ) js) tms)\r
+ else\r
+ problem_fail (finish p) "Finish did not complete the problem"\r
+ ) in try\r
+ aux p\r
+ with Done sigma -> sigma\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 lev = function\r
+ | `Lam(_, t, g) -> L (aux (lev+1) t, List.map (aux (lev+1)) g)\r
+ | `I (v, args) -> Listx.fold_left (fun x y -> fst (mk_app x (aux lev y))) (aux lev (`Var v)) args\r
+ | `Var(v,_) -> if v >= lev && List.nth var_names (v-lev) = "C" then C else 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 -> fst (mk_app x (aux 0 (y :> Num.nf)))) C convs in\r
+ let div = match div with\r
+ | Some div -> aux 0 (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
- sanity p\r
+ {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; label}\r
;;\r
\r
let solve p =\r
- if eta_subterm p.div p.conv\r
- then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
- else check p (auto p)\r
+ let c = if String.length p.label > 0 then String.sub (p.label) 0 1 else "" in\r
+ let module M = struct exception Okay end in\r
+ try\r
+ if eta_subterm p.div p.conv\r
+ then raise (Unseparable "div is subterm of conv")\r
+ else\r
+ let p = sanity p (* initial sanity check *) in\r
+ check p (auto p);\r
+ raise M.Okay\r
+ with\r
+ | M.Okay -> if c = "?" then\r
+ failwith "The problem succeeded, but was supposed to be unseparable"\r
+ | e when c = "!" ->\r
+ failwith ("The problem was supposed to be separable, but: "^Printexc.to_string e)\r
+ | e ->\r
+ print_endline ("The problem failed, as expected ("^Printexc.to_string e^")")\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 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
projects / fireball-separation.git / blobdiff