\r
open Pure\r
\r
+type var_flag = bool ;;\r
+\r
type var = int;;\r
type t =\r
| V of var\r
- | A of t * t\r
+ | A of var_flag * t * t\r
| L of t\r
- | B (* bottom *)\r
- | C of int\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
-\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
-;;\r
-\r
-(* does NOT lift the argument *)\r
-let mk_lams = fold_nat (fun x _ -> L x) ;;\r
-\r
let string_of_t =\r
+ let sep_of_app b = if b then " +" else " " in\r
let string_of_bvar =\r
let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
let bvarsno = List.length bound_vars in\r
- fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in\r
+ fun nn -> if nn < bvarsno then List.nth bound_vars nn else "v" ^ (string_of_int (nn - bvarsno + 1)) 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
+ | 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
in string_of_term_no_pars 0\r
;;\r
\r
+(* does NOT lift the argument *)\r
+let mk_lams = fold_nat (fun x _ -> L x) ;;\r
+\r
+let measure_of_t =\r
+ let rec aux = function\r
+ | V _ -> 0\r
+ | A(b,t1,t2) ->\r
+ (if b then 1 else 0) + aux t1 + aux t2\r
+ | L t -> aux t\r
+ in aux\r
+;;\r
+\r
type problem = {\r
orig_freshno: int\r
; freshno : int\r
- ; div : t\r
- ; conv : t\r
+ ; tms : t list\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
+ let measure = List.fold_left (+) 0 (List.map measure_of_t p.tms) in\r
+ let lines = ("[measure] " ^ string_of_int measure) ::\r
+ List.map (fun x -> "[TM] " ^ string_of_t x) p.tms in\r
String.concat "\n" lines\r
;;\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
+\r
+let rec erase = function\r
+ | L t -> L (erase t)\r
+ | A(_,t1,t2) -> A(false, erase t1, erase t2)\r
+ | V _ as t -> t\r
+;;\r
+\r
+let explode =\r
+ let rec aux args = function\r
+ | L _ -> assert false\r
+ | V _ as x -> x, args\r
+ | A(b,t1,t2) -> aux ((b,t2)::args) t1\r
+ in aux []\r
+;;\r
+\r
+let rec implode hd args =\r
+ match args with\r
+ | [] -> hd\r
+ | (f,a)::args -> implode (A(f,hd,a)) args\r
+;;\r
+\r
+let get_head =\r
+ let rec aux lev = function\r
+ | L t -> aux (lev+1) t\r
+ | A(_,t,_) -> aux lev t\r
+ | V v -> v - lev\r
+ in aux 0\r
;;\r
-let rec subst level delift sub =\r
+\r
+let rec subst level delift ((var, tm) as 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
- else match t1 with\r
- | C _ as t -> t\r
- | B -> B\r
+ | V v -> if v = level + var then lift level tm else V (if delift && v > level then v-1 else v)\r
+ | L t -> L (subst (level + 1) delift sub t)\r
+ | A(b,t1,t2) ->\r
+ let t1' = subst level delift sub t1 in\r
+ let t2' = subst level delift sub t2 in\r
+ mk_app b t1' t2'\r
+and mk_app flag t1 t2 = match t1 with\r
| L t1 -> subst 0 true (0, t2) t1\r
- | _ -> A (t1, t2)\r
+ | _ -> A (flag, 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 t -> L(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 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 mk_app = mk_app true;; *)\r
+let rec mk_apps t = function\r
+ | [] -> t\r
+ | (f,x)::xs -> mk_apps (mk_app f t x) xs\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
+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(false,lift 1 t2,V 0))\r
+ | t1, L t2 -> aux (A(false,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) 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
+ | A(_, t1, t2) -> aux lev t1 || aux lev t2\r
+ | _ -> false\r
in aux 0\r
;;\r
\r
+let subst_in_problem ?(top=true) ((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 sub = (v, t) in\r
+ let tms = List.map (subst sub) p.tms in\r
+ {p with tms; sigma}\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
+ | 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
- print_endline "Checking...";\r
- let div = purify p.div in\r
- let conv = purify p.conv in\r
+ assert false (* FIXME *)\r
+ (* print_endline "Checking...";\r
+ let tms = List.map purify p.tms 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
- ()\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
+ let rec all_different = function\r
+ | [] -> true\r
+ | x::xs -> List.for_all ((<>) x) xs && all_different xs in\r
+ if List.for_all is_var p.tms && all_different p.tms\r
+ then raise (Done p.sigma);\r
+ if List.exists (not ++ is_inert) p.tms\r
+ then problem_fail p "used a non-effective path";\r
p\r
;;\r
\r
-(* drops the arguments of t after the n-th *)\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 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
-;;\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
- 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
- | 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
+let step var j n p =\r
+ let atsnd f (a,b) = (a, f b) in\r
+ let p, alphas = (* make fresh vars *)\r
+ fold_nat (fun (p, vs) _ ->\r
+ let p, v = freshvar p in\r
+ p, v::vs\r
+ ) (p, []) n in let alphas = List.rev alphas in\r
+ let rec aux lev (inside:bool) = function\r
+ | L t -> L (aux (lev+1) inside t)\r
+ | _ as x ->\r
+ let hd, args = explode x in\r
+ if hd = V (var+lev) then\r
+ (let nargs = List.length args in\r
+ let k = max 0 (j + 1 - nargs) in\r
+ let args = List.mapi\r
+ (fun i (f, t) -> f, lift k (aux lev (if i=j then true else inside) t)) args in\r
+ let bound = fold_nat (fun x n -> (false,V(n-1)) :: x) [] k in\r
+ let args = args @ bound in\r
+ let _, head = List.nth args j in\r
+ let args = List.mapi\r
+ (fun i (f, t) -> (if i=j && not inside then false else f), if i=j && not inside then erase t else t) args in\r
+ let head = (if inside then erase else id) head in\r
+ print_endline ("HEAD: " ^ string_of_t head);\r
+ let alphas = List.map (fun v -> false, V(lev+k+v)) alphas in\r
+ let t = mk_apps head (alphas @ args) in\r
+ let t = mk_lams t k in\r
+ t\r
+ ) else\r
+ (let args = List.map (atsnd (aux lev inside)) args in\r
+ implode hd args) in\r
+ let sigma = (var, aux 0 false (V var)) :: p.sigma in\r
+ {p with tms=List.map (aux 0 false) p.tms; sigma}\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 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, 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 = 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
+let finish p = assert false ;;\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
+let rec auto p = assert false ;;\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
-;;\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 (aux t)\r
+ | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app true x (aux y)) (V v) args\r
+ | `Var(v,_) -> V v\r
+ | `N _ | `Match _ -> assert false in\r
+ let convs = (List.rev convs :> Num.nf list) in\r
+ let tms = List.map aux (convs @ (ps :> Num.nf list)) in\r
+ let tms = match div with\r
+ | Some div -> aux (div :> Num.nf) :: tms\r
+ | None -> tms 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; tms; sigma=[]} in\r
(* initial sanity check *)\r
sanity p\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 rec interactive p =\r
+ print_string "[varno index alphano] ";\r
+ let s = read_line () in\r
+ let spl = Str.split (Str.regexp " +") s in\r
+ let nth n = int_of_string (List.nth spl n) in\r
+ let p = step (nth 0) (nth 1) (nth 2) p in\r
+ interactive (sanity p)\r
;;\r
\r
-let run x y = solve (problem_of x y);;\r
-\r
-(* Example usage of interactive: *)\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
-(* 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
+let solve p =\r
+ let rec aux = function\r
+ | [] -> false\r
+ | x::xs -> List.exists (eta_subterm x) xs || aux xs in\r
+ if aux p.tms\r
+ then print_endline "!!! Problem stopped: subterm problem !!!"\r
+ else check p (interactive p)\r
;;\r
\r
-print_hline();\r
-print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r
+Problems.main (solve ++ problem_of);\r
projects / fireball-separation.git / blobdiff