type var = int;;\r
type t =\r
| V of var\r
- | A of t * t\r
- | L of t\r
- | B (* bottom *)\r
- | C of int\r
+ | A of (bool ref) * t * t\r
+ | L of (bool * t)\r
;;\r
\r
-let delta = L(A(V 0, V 0));;\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
- | 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
-let eta_eq = eta_eq' 0 0;;\r
+let measure_of_t =\r
+ let rec aux acc = function\r
+ | V _ -> acc, 0\r
+ | A(b,t1,t2) ->\r
+ let acc, m1 = aux acc t1 in\r
+ let acc, m2 = aux acc t2 in\r
+ if not (List.memq b acc) && !b then b::acc, 1 + m1 + m2 else acc, m1 + m2\r
+ | L(b,t) -> if b then aux acc t else acc, 0\r
+ in snd ++ (aux [])\r
+;;\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
- | A(t1, t2) -> aux lev t1 || aux lev t2\r
- | _ -> false\r
- in aux 0\r
+let index_of x =\r
+ let rec aux n =\r
+ function\r
+ [] -> None\r
+ | x'::_ when x == x' -> Some n\r
+ | _::xs -> aux (n+1) xs\r
+ in aux 1\r
;;\r
\r
-(* does NOT lift the argument *)\r
-let mk_lams = fold_nat (fun x _ -> L x) ;;\r
+let sep_of_app =\r
+ let apps = ref [] in\r
+ function\r
+ r when not !r -> " "\r
+ | r ->\r
+ let i =\r
+ match index_of r !apps with\r
+ Some i -> i\r
+ | None ->\r
+ apps := !apps @ [r];\r
+ List.length !apps\r
+ in " " ^ string_of_int i ^ ":"\r
+;;\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
| 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
+ | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ sep_of_app b ^ 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) -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r
| _ as t -> string_of_term_no_pars_app level t\r
in string_of_term_no_pars 0\r
;;\r
\r
+\r
+let delta = L(true,A(ref true,V 0, V 0));;\r
+\r
+(* does NOT lift the argument *)\r
+let mk_lams = fold_nat (fun x _ -> L(false,x)) ;;\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
; 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
+ "[measure] " ^ string_of_int (measure_of_t p.div);\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
\r
let rec is_inert =\r
function\r
- | A(t,_) -> is_inert t\r
+ | A(_,t,_) -> is_inert t\r
| V _ -> true\r
- | C _\r
- | L _ | B -> false\r
+ | L _ -> false\r
;;\r
\r
let is_var = function V _ -> true | _ -> false;;\r
\r
let rec get_inert = function\r
| V n -> (n,0)\r
- | A(t, _) -> let hd,args = get_inert t in hd,args+1\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' then max 0 (n - m) else 0\r
+ | V v' -> if v = v' then n else 0\r
;;\r
-let rec subst level delift sub =\r
+\r
+(* b' is true iff we are substituting the argument of a step\r
+ and the application of the redex was true. Therefore we need to\r
+ set the new app to true. *)\r
+let rec subst b' 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
- | 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
+ | L(b,t) -> L(b, subst b' (level + 1) delift sub t)\r
+ | A(_,t1,(V v as t2)) when b' && v = level + fst sub ->\r
+ mk_app (ref true) (subst b' level delift sub t1) (subst b' level delift sub t2)\r
+ | A(b,t1,t2) ->\r
+ mk_app b (subst b' level delift sub t1) (subst b' level delift sub t2)\r
+(* b is\r
+ - a fresh ref true if we want to create a real application from scratch\r
+ - a shared ref true if we substituting in the head of a real application *)\r
+and mk_app b' 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(b,t1) ->\r
+ let last_lam = match t1 with L _ -> false | _ -> true in\r
+ if not b && last_lam then b' := false ;\r
+ subst (!b' && not b && not last_lam) 0 true (0, t2) t1\r
+ | _ -> A (b', 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
- | A (t1, t2) -> A (aux lev t1, aux lev t2)\r
- | C _ as t -> t\r
- | B -> B\r
+ | L(b,t) -> L(b,aux (lev+1) t)\r
+ | A (b,t1, t2) -> A (b,aux lev t1, aux lev t2)\r
+ in aux 0\r
+;;\r
+let subst = subst false 0 false;;\r
+let mk_app t1 = mk_app (ref true) t1;;\r
+\r
+let eta_eq =\r
+ let rec aux t1 t2 = match t1, t2 with\r
+ | L(_,t1), L(_,t2) -> aux t1 t2\r
+ | L(_,t1), t2 -> aux t1 (A(ref true,lift 1 t2,V 0))\r
+ | t1, L(_,t2) -> aux (A(ref true,lift 1 t1,V 0)) t2\r
+ | V a, V b -> a = b\r
+ | A(_,t1,t2), A(_,u1,u2) -> aux t1 u1 && aux 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 u (lift lev 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
;;\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
+\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 = try subst sub p.div with B -> raise (Done sigma) in\r
+ let conv = try subst sub p.conv with B -> raise (Fail(-1,"p.conv diverged")) in\r
+ {p with div; conv; 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
- | A(t1,t2) as t ->\r
+ | V _ -> None\r
+ | L(_,t) -> aux (lev+1) 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
+ (* the `+1` above is because of t2 *)\r
then Some (lift ~-lev t)\r
else match aux lev t2 with\r
| None -> aux lev t1\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
+ | 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
;;\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
p\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
| V _ as t -> 0, t\r
- | A(t1,_) as 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
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
- | 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
+ | V _, V _ -> None\r
+ | A(_,t1,t2), A(_,u1,u2) ->\r
+ (match aux t1 u1 (k-1) with\r
+ | None ->\r
+ if not (eta_eq t2 u2) then Some (k-1)\r
+ else None\r
+ | Some j -> Some j)\r
| _, _ -> assert false\r
- in aux p.div t n_args\r
+ in match aux p.div t argsno with\r
+ | None -> problem_fail p "no eta difference found (div subterm of conv?)"\r
+ | Some j -> j\r
;;\r
\r
let compute_max_lambdas_at hd_var j =\r
let rec aux hd = function\r
- | A(t1,t2) ->\r
+ | A(_,t1,t2) ->\r
(if get_inert t1 = (hd, j)\r
then max ( (*FIXME*)\r
if is_inert t2 && let hd', j' = get_inert t2 in hd' = 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
+ | L(_,t) -> aux (hd+1) t\r
| V _ -> 0\r
- | _ -> assert false\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
-;;\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
let p, t = (* apply fresh vars *)\r
fold_nat (fun (p, t) _ ->\r
let p, v = freshvar p in\r
- p, A(t, V (v + k + 1))\r
+ p, A(ref false, t, V (v + k + 1))\r
) (p, V 0) n in\r
- let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
- fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
+ let t = (* apply bound variables V_k..V_0 *)\r
+ fold_nat (fun t m -> A(ref false, t, V (k-m+1))) t (k+1) 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
-;;\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
+ 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
+ | V _ -> n\r
+ in aux 0 in\r
+print_cmd "FINISH" "";\r
+ let div_hd, div_nargs = get_inert p.div 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
+ let div_hd, div_nargs = get_inert p.div in\r
+ let rec aux m = function\r
+ A(_,t1,t2) -> if is_var t2 then\r
+ (let delta_var, _ = get_inert t2 in\r
+ if delta_var <> div_hd && get_subterm_with_head_and_args delta_var 1 p.conv = None\r
+ then m, delta_var\r
+ else aux (m-1) t1) else aux (m-1) t1\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 problem_fail (finish p) "Auto.2 did not complete the problem"\r
+ with Done sigma -> sigma)\r
+ (*\r
(try\r
let phase = p.phase in\r
let p = eat p in\r
then problem_fail p "Auto.2 did not complete the problem"\r
else auto p\r
with Done sigma -> sigma)\r
+ *)\r
| Some t ->\r
- let j = find_eta_difference p t n_args - 1 in\r
+ let j = find_eta_difference p t n_args 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 m1 = measure_of_t p.div in\r
let p = step j k p in\r
+ let m2 = measure_of_t p.div in\r
+ (if m2 >= m1 then\r
+ (print_string ("WARNING! Measure did not decrease : " ^ string_of_int m2 ^ " >= " ^ string_of_int m1 ^ " (press <Enter>)");\r
+ ignore(read_line())));\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 (true,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 :> Num.nf list) in\r
+ let conv = aux\r
+ (if List.length convs = 1\r
+ then List.hd convs\r
+ else `I((List.length var_names, min_int), Listx.from_list 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
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; phase=`One} in\r
(* initial sanity check *)\r
sanity p\r
;;\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 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