| 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
function\r
| A(t,_) -> is_inert t\r
| V _ -> true\r
- | C _\r
+ | C\r
| L _ | B -> false\r
;;\r
\r
-let is_var = function V _ -> true | _ -> false;;\r
-let is_lambda = function L _ -> true | _ -> false;;\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
+(* 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
+ | B | 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
+ | C | B as t -> t\r
and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
else match t1 with\r
| B -> B\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 | B as t -> t\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
+ stepped=v::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
+ | C | V _ | B -> []\r
+ | L t -> aux (lev+1) false t\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
+ | C -> Pure.V (min_int/2)\r
| B -> Pure.B\r
;;\r
\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
\r
(* drops the arguments of t after the n-th *)\r
+(* FIXME! E' usato in modo improprio contando sul fatto\r
+ errato che ritorna un inerte lungo esattamente n *)\r
let inert_cut_at n t =\r
let rec aux t =\r
match t with\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
+(* return the index of the first argument with a difference\r
+ (the first argument is 0)\r
+ precondition: p.div and t have n+1 arguments\r
+ *)\r
+let find_eta_difference p t argsno =\r
+ let t = inert_cut_at argsno t in\r
let rec aux t u k = match t, u with\r
- | V _, V _ -> assert false (* div subterm of conv *)\r
+ | V _, V _ -> []\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
+ print_endline (string_of_t t2 ^ " vs " ^ string_of_t u2);\r
+ if not (eta_eq t2 u2) then (k-1)::aux t1 u1 (k-1)\r
else aux t1 u1 (k-1)\r
| _, _ -> assert false\r
- in aux p.div t n_args\r
+ in aux p.div t argsno\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
+ | V _ | C -> 0\r
| _ -> assert false\r
in aux hd_var\r
;;\r
let eat p =\r
print_cmd "EAT" "";\r
let var, k = get_inert p.div in\r
+ match var with\r
+ | C | L _ | B | A _ -> assert false\r
+ | V var ->\r
let phase = p.phase in\r
let p =\r
match phase with\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 _ | B | 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
-;;\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 auto p =\r
+ let rec aux p =\r
+ let hd, n_args = get_inert p.div in\r
+ match hd with\r
+ | C | L _ | B | 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 n_args 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
+ (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
+ else aux p)\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 -> 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 -> 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
;;\r
\r
let solve p =\r
- if eta_subterm p.div p.conv\r
+ if is_stuck p.div 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
;;\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