| _ -> 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
+(* 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
| B | 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
;;\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
| 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
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 _ -> problem_fail p "no eta difference found (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
+ if not (eta_eq t2 u2) then (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
print_cmd "EAT" "";\r
let var, k = get_inert p.div in\r
let phase = p.phase in\r
- let p, t =\r
+ let p =\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
+ (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 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
+ 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
;;\r
\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
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 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
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 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 in\r
+ let conv = List.fold_left (fun x y -> mk_app x (aux (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 (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
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