ocaml/simple.ml

   1 let (++) f g x = f (g x);;\r
   2 let id x = x;;\r
   3 let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;\r
   4 \r
   5 let print_hline = Console.print_hline;;\r
   6 \r
   7 open Pure\r
   8 \r
   9 type var = int;;\r
  10 type t =\r
  11  | V of var\r
  12  | A of t * t\r
  13  | L of t\r
  14  | B (* bottom *)\r
  15  | C of int\r
  16 ;;\r
  17 \r
  18 let delta = L(A(V 0, V 0));;\r
  19 \r
  20 let eta_eq' =\r
  21  let rec aux l1 l2 t1 t2 = match t1, t2 with\r
  22   | L t1, L t2 -> aux l1 l2 t1 t2\r
  23   | L t1, t2 -> aux l1 (l2+1) t1 t2\r
  24   | t1, L t2 -> aux (l1+1) l2 t1 t2\r
  25   | V a, V b -> a + l1 = b + l2\r
  26   | C a, C b -> a = b\r
  27   | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2\r
  28   | _, _ -> false\r
  29  in aux ;;\r
  30 let eta_eq = eta_eq' 0 0;;\r
  31 \r
  32 (* is arg1 eta-subterm of arg2 ? *)\r
  33 let eta_subterm u =\r
  34  let rec aux lev t = eta_eq' lev 0 u t || match t with\r
  35  | L t -> aux (lev+1) t\r
  36  | A(t1, t2) -> aux lev t1 || aux lev t2\r
  37  | _ -> false\r
  38  in aux 0\r
  39 ;;\r
  40 \r
  41 (* does NOT lift the argument *)\r
  42 let mk_lams = fold_nat (fun x _ -> L x) ;;\r
  43 \r
  44 let string_of_t =\r
  45   let string_of_bvar =\r
  46    let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
  47    let bvarsno = List.length bound_vars in\r
  48    fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in\r
  49   let rec string_of_term_w_pars level = function\r
  50     | V v -> if v >= level then "`" ^ string_of_int (v-level) else\r
  51        string_of_bvar (level - v-1)\r
  52     | C n -> "c" ^ string_of_int n\r
  53     | A _\r
  54     | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
  55     | B -> "BOT"\r
  56   and string_of_term_no_pars_app level = function\r
  57     | A(t1,t2) -> string_of_term_no_pars_app level t1 ^ " " ^ string_of_term_w_pars level t2\r
  58     | _ as t -> string_of_term_w_pars level t\r
  59   and string_of_term_no_pars level = function\r
  60     | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r
  61     | _ as t -> string_of_term_no_pars_app level t\r
  62   in string_of_term_no_pars 0\r
  63 ;;\r
  64 \r
  65 type problem = {\r
  66    orig_freshno: int\r
  67  ; freshno : int\r
  68  ; div : t\r
  69  ; conv : t\r
  70  ; sigma : (var * t) list (* substitutions *)\r
  71  ; stepped : var list\r
  72  ; phase : [`One | `Two] (* :'( *)\r
  73 }\r
  74 \r
  75 let string_of_problem p =\r
  76  let lines = [\r
  77   "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);\r
  78   "[DV] " ^ string_of_t p.div;\r
  79   "[CV] " ^ string_of_t p.conv;\r
  80  ] in\r
  81  String.concat "\n" lines\r
  82 ;;\r
  83 \r
  84 exception Done of (var * t) list (* substitution *);;\r
  85 exception Fail of int * string;;\r
  86 \r
  87 let problem_fail p reason =\r
  88  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
  89  print_endline (string_of_problem p);\r
  90  raise (Fail (-1, reason))\r
  91 ;;\r
  92 \r
  93 let freshvar ({freshno} as p) =\r
  94  {p with freshno=freshno+1}, freshno+1\r
  95 ;;\r
  96 \r
  97 let rec is_inert =\r
  98  function\r
  99  | A(t,_) -> is_inert t\r
 100  | V _ -> true\r
 101  | C _\r
 102  | L _ | B -> false\r
 103 ;;\r
 104 \r
 105 let is_var = function V _ -> true | _ -> false;;\r
 106 let is_lambda = function L _ -> true | _ -> false;;\r
 107 \r
 108 let rec get_inert = function\r
 109  | V n -> (n,0)\r
 110  | A(t, _) -> let hd,args = get_inert t in hd,args+1\r
 111  | _ -> assert false\r
 112 ;;\r
 113 \r
 114 let rec no_leading_lambdas hd_var j = function\r
 115  | L t -> 1 + no_leading_lambdas (hd_var+1) j t\r
 116  | A _ as t -> let hd_var', n = get_inert t in if hd_var = hd_var' then max 0 (j - n) else 0\r
 117  | V n -> if n = hd_var then j else 0\r
 118  | B | C _ -> 0\r
 119 ;;\r
 120 let rec subst level delift sub =\r
 121  function\r
 122  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
 123  | L t -> let t = subst (level + 1) delift sub t in if t = B then B else L t\r
 124  | A (t1,t2) ->\r
 125   let t1 = subst level delift sub t1 in\r
 126   let t2 = subst level delift sub t2 in\r
 127   mk_app t1 t2\r
 128  | C _ as t -> t\r
 129  | B -> B\r
 130 and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
 131  else match t1 with\r
 132  | B -> B\r
 133  | L t1 -> subst 0 true (0, t2) t1\r
 134  | _ -> A (t1, t2)\r
 135 and lift n =\r
 136  let rec aux lev =\r
 137   function\r
 138   | V m -> V (if m >= lev then m + n else m)\r
 139   | L t -> L (aux (lev+1) t)\r
 140   | A (t1, t2) -> A (aux lev t1, aux lev t2)\r
 141   | C _ as t -> t\r
 142   | B -> B\r
 143  in aux 0\r
 144 ;;\r
 145 let subst = subst 0 false;;\r
 146 \r
 147 let subst_in_problem sub p =\r
 148 print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));\r
 149  {p with\r
 150   div=subst sub p.div;\r
 151   conv=subst sub p.conv;\r
 152   stepped=(fst sub)::p.stepped;\r
 153   sigma=sub::p.sigma}\r
 154 ;;\r
 155 \r
 156 let get_subterm_with_head_and_args hd_var n_args =\r
 157  let rec aux lev = function\r
 158  | C _\r
 159  | V _ | B -> None\r
 160  | L t -> aux (lev+1) t\r
 161  | A(t1,t2) as t ->\r
 162    let hd_var', n_args' = get_inert t1 in\r
 163    if hd_var' = hd_var + lev && n_args <= 1 + n_args'\r
 164     then Some (lift ~-lev t)\r
 165     else match aux lev t2 with\r
 166     | None -> aux lev t1\r
 167     | Some _ as res -> res\r
 168  in aux 0\r
 169 ;;\r
 170 \r
 171 let rec purify = function\r
 172  | L t -> Pure.L (purify t)\r
 173  | A (t1,t2) -> Pure.A (purify t1, purify t2)\r
 174  | V n -> Pure.V n\r
 175  | C _ -> Pure.V max_int (* FIXME *)\r
 176  | B -> Pure.B\r
 177 ;;\r
 178 \r
 179 let check p sigma =\r
 180  print_endline "Checking...";\r
 181  let div = purify p.div in\r
 182  let conv = purify p.conv in\r
 183  let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r
 184  let freshno = List.fold_right (fun (x,_) -> max x) sigma 0 in\r
 185  let env = Pure.env_of_sigma freshno sigma in\r
 186  assert (Pure.diverged (Pure.mwhd (env,div,[])));\r
 187  print_endline " D diverged.";\r
 188  assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));\r
 189  print_endline " C converged.";\r
 190  ()\r
 191 ;;\r
 192 \r
 193 let sanity p =\r
 194  print_endline (string_of_problem p); (* non cancellare *)\r
 195  if p.conv = B then problem_fail p "p.conv diverged";\r
 196  if p.div = B then raise (Done p.sigma);\r
 197  if p.phase = `Two && p.div = delta then raise (Done p.sigma);\r
 198  if not (is_inert p.div) then problem_fail p "p.div converged";\r
 199  p\r
 200 ;;\r
 201 \r
 202 (* drops the arguments of t after the n-th *)\r
 203 let inert_cut_at n t =\r
 204  let rec aux t =\r
 205   match t with\r
 206   | V _ as t -> 0, t\r
 207   | A(t1,_) as t ->\r
 208     let k', t' = aux t1 in\r
 209      if k' = n then n, t'\r
 210       else k'+1, t\r
 211   | _ -> assert false\r
 212  in snd (aux t)\r
 213 ;;\r
 214 \r
 215 let find_eta_difference p t n_args =\r
 216  let t = inert_cut_at n_args t in\r
 217  let rec aux t u k = match t, u with\r
 218  | V _, V _ -> assert false (* div subterm of conv *)\r
 219  | A(t1,t2), A(u1,u2) ->\r
 220     if not (eta_eq t2 u2) then ((*print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2));*) k)\r
 221     else aux t1 u1 (k-1)\r
 222  | _, _ -> assert false\r
 223  in aux p.div t n_args\r
 224 ;;\r
 225 \r
 226 let compute_max_lambdas_at hd_var j =\r
 227  let rec aux hd = function\r
 228  | A(t1,t2) ->\r
 229     (if get_inert t1 = (hd, j)\r
 230       then max ( (*FIXME*)\r
 231        if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd\r
 232         then let hd', j' = get_inert t2 in j - j'\r
 233         else no_leading_lambdas hd_var j t2)\r
 234       else id) (max (aux hd t1) (aux hd t2))\r
 235  | L t -> aux (hd+1) t\r
 236  | V _ -> 0\r
 237  | _ -> assert false\r
 238  in aux hd_var\r
 239 ;;\r
 240 \r
 241 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 242 \r
 243 (* eat the arguments of the divergent and explode.\r
 244  It does NOT perform any check, may fail if done unsafely *)\r
 245 let eat p =\r
 246 print_cmd "EAT" "";\r
 247  let var, k = get_inert p.div in\r
 248  let phase = p.phase in\r
 249  let p =\r
 250   match phase with\r
 251   | `One ->\r
 252       let n = 1 + max\r
 253        (compute_max_lambdas_at var (k-1) p.div)\r
 254        (compute_max_lambdas_at var (k-1) p.conv) in\r
 255       (* apply fresh vars *)\r
 256       let p, t = fold_nat (fun (p, t) _ ->\r
 257         let p, v = freshvar p in\r
 258         p, A(t, V (v + k))\r
 259       ) (p, V 0) n in\r
 260       let p = {p with phase=`Two} in\r
 261       let t = A(t, delta) in\r
 262       let t = fold_nat (fun t m -> A(t, V (k-m))) t (k-1) in\r
 263       let subst = var, mk_lams t k in\r
 264       let p = subst_in_problem subst p in\r
 265       let _, args = get_inert p.div in\r
 266       {p with div = inert_cut_at (args-k) p.div}\r
 267   | `Two ->\r
 268       let subst = var, mk_lams delta k in\r
 269       subst_in_problem subst p in\r
 270  sanity p\r
 271 ;;\r
 272 \r
 273 (* step on the head of div, on the k-th argument, with n fresh vars *)\r
 274 let step k n p =\r
 275  let var, _ = get_inert p.div in\r
 276 print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 277  let p, t = (* apply fresh vars *)\r
 278   fold_nat (fun (p, t) _ ->\r
 279     let p, v = freshvar p in\r
 280     p, A(t, V (v + k + 1))\r
 281   ) (p, V 0) n in\r
 282  let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
 283   fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
 284  let t = mk_lams t (k+1) in (* make leading lambdas *)\r
 285  let subst = var, t in\r
 286  let p = subst_in_problem subst p in\r
 287  sanity p\r
 288 ;;\r
 289 ;;\r
 290 \r
 291 let parse strs =\r
 292   let rec aux level = function\r
 293   | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
 294   | Parser_andrea.App (t1, t2) ->\r
 295    if level = 0 then mk_app (aux level t1) (aux level t2)\r
 296     else A(aux level t1, aux level t2)\r
 297   | Parser_andrea.Var v -> V v in\r
 298   let (tms, free) = Parser_andrea.parse_many strs in\r
 299   (List.map (aux 0) tms, free)\r
 300 ;;\r
 301 \r
 302 let rec auto p =\r
 303  let hd_var, n_args = get_inert p.div in\r
 304  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
 305  | None ->\r
 306    (try\r
 307     let phase = p.phase in\r
 308      let p = eat p in\r
 309      if phase = `Two\r
 310       then problem_fail p "Auto.2 did not complete the problem"\r
 311       else auto p\r
 312     with Done sigma -> sigma)\r
 313  | Some t ->\r
 314   let j = find_eta_difference p t n_args - 1 in\r
 315   let k = 1 + max\r
 316    (compute_max_lambdas_at hd_var j p.div)\r
 317     (compute_max_lambdas_at hd_var j p.conv) in\r
 318   let p = step j k p in\r
 319   auto p\r
 320 ;;\r
 321 \r
 322 let problem_of div convs =\r
 323  let rec conv_join = function\r
 324   | [] -> "@"\r
 325   | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
 326  print_hline ();\r
 327  let conv = conv_join convs in\r
 328  let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
 329  let varno = List.length var_names in\r
 330  let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
 331  (* initial sanity check *)\r
 332  sanity p\r
 333 ;;\r
 334 \r
 335 let solve p =\r
 336  if eta_subterm p.div p.conv\r
 337   then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
 338   else check p (auto p)\r
 339 ;;\r
 340 \r
 341 let run x y = solve (problem_of x y);;\r
 342 \r
 343 (* Example usage of interactive: *)\r
 344 \r
 345 (* let interactive div conv cmds =\r
 346  let p = problem_of div conv in\r
 347  try (\r
 348  let p = List.fold_left (|>) p cmds in\r
 349  let rec f p cmds =\r
 350   let nth spl n = int_of_string (List.nth spl n) in\r
 351   let read_cmd () =\r
 352    let s = read_line () in\r
 353    let spl = Str.split (Str.regexp " +") s in\r
 354    s, let uno = List.hd spl in\r
 355     try if uno = "eat" then eat\r
 356     else if uno = "step" then step (nth spl 1) (nth spl 2)\r
 357     else failwith "Wrong input."\r
 358     with Failure s -> print_endline s; (fun x -> x) in\r
 359   let str, cmd = read_cmd () in\r
 360   let cmds = (" " ^ str ^ ";")::cmds in\r
 361   try\r
 362    let p = cmd p in f p cmds\r
 363   with\r
 364   | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
 365  in f p []\r
 366  ) with Done _ -> ()\r
 367 ;; *)\r
 368 \r
 369 (* interactive "x y"\r
 370  "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
 371 ;; *)\r
 372 \r
 373 run "x x" ["x y"; "y y"; "y x"] ;;\r
 374 run "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
 375 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
 376 \r
 377 run "x (y. x y y)" ["x (y. x y x)"] ;;\r
 378 \r
 379 run "x a a a a" [\r
 380  "x b a a a";\r
 381  "x a b a a";\r
 382  "x a a b a";\r
 383  "x a a a b";\r
 384 ] ;;\r
 385 \r
 386 (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
 387 run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
 388  "x a a a a (_. a) b b b";\r
 389  "x a a a a (_. _. _. _. x. y. x y)";\r
 390 ] ;;\r
 391 \r
 392 (* bug in eat that was erasing terms in convergent that then diverged *)\r
 393 run "x y z"\r
 394 [\r
 395 "x @ @";\r
 396 "z (y @ (y @))"\r
 397 ] ;;\r
 398 \r
 399 (* bug in no_leading_lambdas where x in j-th position *)\r
 400 run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
 401 ["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
 402 ;;\r
 403 \r
 404 print_hline();\r
 405 print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r