| V of var\r
| A of t * t\r
| L of t\r
- | B (* bottom *)\r
- | C of int\r
+ | C (* constant *)\r
;;\r
\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
+ | _, _ when is_stuck t1 || is_stuck t2 -> true\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
- | 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
+ let rec aux lev t = if t = C then false else (eta_eq' lev 0 u t || match t with\r
| L t -> aux (lev+1) t\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 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
; 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
\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
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
+ | C -> C\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
and lift n =\r
| V m -> V (if m >= lev then m + n else m)\r
| L t -> L (aux (lev+1) t)\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
+let subst_in_problem ((v, t) as sub) p =\r
+print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);\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
;;\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 get_subterms_with_head hd_var =\r
+ let rec aux lev inert_done = function\r
+ | L t -> aux (lev+1) false t\r
+ | C | V _ -> []\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 true t1 @ aux lev false t2\r
+ else aux lev true t1 @ aux lev false 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
+ | C -> Pure.V (min_int/2)\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
\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 aux k divargs conargs =\r
+ match divargs,conargs with\r
+ [],_ -> []\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
+ | 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 =\r
- match phase with\r
- | `One ->\r
- let n = 1 + max\r
- (compute_max_lambdas_at var (k-1) p.div)\r
- (compute_max_lambdas_at var (k-1) 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\r
- let t = A(t, delta) in\r
- let t = fold_nat (fun t m -> A(t, V (k-m))) t (k-1) in\r
- let subst = var, mk_lams t k in\r
- let p = subst_in_problem subst p in\r
- let _, args = get_inert p.div in\r
- {p with div = inert_cut_at (args-k) p.div}\r
- | `Two ->\r
- let subst = var, mk_lams delta k in\r
- subst_in_problem subst 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
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
+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 -> max n (aux 0 t)\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
+ 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
+ List.iter (fun t -> try\r
+ let js = find_eta_difference p t in\r
+ (* print_endline (String.concat ", " (List.map string_of_int js)); *)\r
+ if js = [] then problem_fail p "no eta difference found (div subterm of conv?)";\r
+ let js = List.rev js in\r
+ List.iter\r
+ (fun j ->\r
+ try\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
+ ignore (aux (step j k p))\r
+ with Fail(_, s) ->\r
+ print_endline ("Backtracking (eta_diff) because: " ^ s)) js;\r
+ raise (Fail(-1, "no eta difference"))\r
+ with Fail(_, s) ->\r
+ print_endline ("Backtracking (get_subterms) because: " ^ s)) tms;\r
+ raise (Fail(-1, "no similar terms"))\r
+ )\r
+ else\r
+ problem_fail (finish p) "Finish did not complete the problem"\r
+ in\r
+ 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) -> L (aux (lev+1) t, [])\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)))) (V (List.length var_names)) convs in\r
+ let var_names = "@" :: var_names 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=[]}\r
;;\r
\r
let solve p =\r
- if eta_subterm p.div p.conv\r
+ if is_constant p.div\r
+ then print_endline "!!! div is stuck. Problem was not run !!!"\r
+ else 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
+ else let p = sanity p (* initial sanity check *) in 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
projects / fireball-separation.git / blobdiff