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 \r
 121 let rec subst level delift sub =\r
 122  function\r
 123  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
 124  | L t -> let t = subst (level + 1) delift sub t in if t = B then B else L t\r
 125  | A (t1,t2) ->\r
 126   let t1 = subst level delift sub t1 in\r
 127   let t2 = subst level delift sub t2 in\r
 128   mk_app t1 t2\r
 129  | C _ as t -> t\r
 130  | B -> B\r
 131 and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
 132  else match t1 with\r
 133  | B -> B\r
 134  | L t1 -> subst 0 true (0, t2) t1\r
 135  | _ -> A (t1, t2)\r
 136 and lift n =\r
 137  let rec aux lev =\r
 138   function\r
 139   | V m -> V (if m >= lev then m + n else m)\r
 140   | L t -> L (aux (lev+1) t)\r
 141   | A (t1, t2) -> A (aux lev t1, aux lev t2)\r
 142   | C _ as t -> t\r
 143   | B -> B\r
 144  in aux 0\r
 145 ;;\r
 146 let subst = subst 0 false;;\r
 147 \r
 148 let subst_in_problem sub p =\r
 149 print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));\r
 150  {p with\r
 151   div=subst sub p.div;\r
 152   conv=subst sub p.conv;\r
 153   stepped=(fst sub)::p.stepped;\r
 154   sigma=sub::p.sigma}\r
 155 ;;\r
 156 \r
 157 let get_subterm_with_head_and_args hd_var n_args =\r
 158  let rec aux lev = function\r
 159  | C _\r
 160  | V _ | B -> None\r
 161  | L t -> aux (lev+1) t\r
 162  | A(t1,t2) as t ->\r
 163    let hd_var', n_args' = get_inert t1 in\r
 164    if hd_var' = hd_var + lev && n_args <= 1 + n_args'\r
 165     then Some (lift ~-lev t)\r
 166     else match aux lev t2 with\r
 167     | None -> aux lev t1\r
 168     | Some _ as res -> res\r
 169  in aux 0\r
 170 ;;\r
 171 \r
 172 let rec purify = function\r
 173  | L t -> Pure.L (purify t)\r
 174  | A (t1,t2) -> Pure.A (purify t1, purify t2)\r
 175  | V n -> Pure.V n\r
 176  | C _ -> Pure.V max_int (* FIXME *)\r
 177  | B -> Pure.B\r
 178 ;;\r
 179 \r
 180 let check p sigma =\r
 181  print_endline "Checking...";\r
 182  let div = purify p.div in\r
 183  let conv = purify p.conv in\r
 184  let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r
 185  let freshno = List.fold_right (fun (x,_) -> max x) sigma 0 in\r
 186  let env = Pure.env_of_sigma freshno sigma in\r
 187  assert (Pure.diverged (Pure.mwhd (env,div,[])));\r
 188  print_endline " D diverged.";\r
 189  assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));\r
 190  print_endline " C converged.";\r
 191  ()\r
 192 ;;\r
 193 \r
 194 let sanity p =\r
 195  print_endline (string_of_problem p); (* non cancellare *)\r
 196  if p.conv = B then problem_fail p "p.conv diverged";\r
 197  if p.div = B then raise (Done p.sigma);\r
 198  if p.phase = `Two && p.div = delta then raise (Done p.sigma);\r
 199  if not (is_inert p.div) then problem_fail p "p.div converged";\r
 200  p\r
 201 ;;\r
 202 \r
 203 (* drops the arguments of t after the n-th *)\r
 204 let inert_cut_at n t =\r
 205  let rec aux t =\r
 206   match t with\r
 207   | V _ as t -> 0, t\r
 208   | A(t1,_) as t ->\r
 209     let k', t' = aux t1 in\r
 210      if k' = n then n, t'\r
 211       else k'+1, t\r
 212   | _ -> assert false\r
 213  in snd (aux t)\r
 214 ;;\r
 215 \r
 216 let find_eta_difference p t n_args =\r
 217  let t = inert_cut_at n_args t in\r
 218  let rec aux t u k = match t, u with\r
 219  | V _, V _ -> assert false (* div subterm of conv *)\r
 220  | A(t1,t2), A(u1,u2) ->\r
 221     if not (eta_eq t2 u2) then ((*print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2));*) k)\r
 222     else aux t1 u1 (k-1)\r
 223  | _, _ -> assert false\r
 224  in aux p.div t n_args\r
 225 ;;\r
 226 \r
 227 let compute_max_lambdas_at hd_var j =\r
 228  let rec aux hd = function\r
 229  | A(t1,t2) ->\r
 230     (if get_inert t1 = (hd, j)\r
 231       then max ( (*FIXME*)\r
 232        if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd\r
 233         then let hd', j' = get_inert t2 in j - j'\r
 234         else no_leading_lambdas hd_var j t2)\r
 235       else id) (max (aux hd t1) (aux hd t2))\r
 236  | L t -> aux (hd+1) t\r
 237  | V _ -> 0\r
 238  | _ -> assert false\r
 239  in aux hd_var\r
 240 ;;\r
 241 \r
 242 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 243 \r
 244 (* eat the arguments of the divergent and explode.\r
 245  It does NOT perform any check, may fail if done unsafely *)\r
 246 let eat p =\r
 247 print_cmd "EAT" "";\r
 248  let var, k = get_inert p.div in\r
 249  let phase = p.phase in\r
 250  let p =\r
 251   match phase with\r
 252   | `One ->\r
 253       let n = 1 + max\r
 254        (compute_max_lambdas_at var (k-1) p.div)\r
 255        (compute_max_lambdas_at var (k-1) p.conv) in\r
 256       (* apply fresh vars *)\r
 257       let p, t = fold_nat (fun (p, t) _ ->\r
 258         let p, v = freshvar p in\r
 259         p, A(t, V (v + k))\r
 260       ) (p, V 0) n in\r
 261       let p = {p with phase=`Two} in\r
 262       let t = A(t, delta) in\r
 263       let t = fold_nat (fun t m -> A(t, V (k-m))) t (k-1) in\r
 264       let subst = var, mk_lams t k in\r
 265       let p = subst_in_problem subst p in\r
 266       let _, args = get_inert p.div in\r
 267       {p with div = inert_cut_at (args-k) p.div}\r
 268   | `Two ->\r
 269       let subst = var, mk_lams delta k in\r
 270       subst_in_problem subst p in\r
 271  sanity p\r
 272 ;;\r
 273 \r
 274 (* step on the head of div, on the k-th argument, with n fresh vars *)\r
 275 let step k n p =\r
 276  let var, _ = get_inert p.div in\r
 277 print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 278  let p, t = (* apply fresh vars *)\r
 279   fold_nat (fun (p, t) _ ->\r
 280     let p, v = freshvar p in\r
 281     p, A(t, V (v + k + 1))\r
 282   ) (p, V 0) n in\r
 283  let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
 284   fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
 285  let t = mk_lams t (k+1) in (* make leading lambdas *)\r
 286  let subst = var, t in\r
 287  let p = subst_in_problem subst p in\r
 288  sanity p\r
 289 ;;\r
 290 ;;\r
 291 \r
 292 let parse strs =\r
 293   let rec aux level = function\r
 294   | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
 295   | Parser_andrea.App (t1, t2) ->\r
 296    if level = 0 then mk_app (aux level t1) (aux level t2)\r
 297     else A(aux level t1, aux level t2)\r
 298   | Parser_andrea.Var v -> V v in\r
 299   let (tms, free) = Parser_andrea.parse_many strs in\r
 300   (List.map (aux 0) tms, free)\r
 301 ;;\r
 302 \r
 303 let rec auto p =\r
 304  let hd_var, n_args = get_inert p.div in\r
 305  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
 306  | None ->\r
 307    (try\r
 308     let phase = p.phase in\r
 309      let p = eat p in\r
 310      if phase = `Two\r
 311       then problem_fail p "Auto.2 did not complete the problem"\r
 312       else auto p\r
 313     with Done sigma -> sigma)\r
 314  | Some t ->\r
 315   let j = find_eta_difference p t n_args - 1 in\r
 316   let k = 1 + max\r
 317    (compute_max_lambdas_at hd_var j p.div)\r
 318     (compute_max_lambdas_at hd_var j p.conv) in\r
 319   let p = step j k p in\r
 320   auto p\r
 321 ;;\r
 322 \r
 323 let problem_of div convs =\r
 324  let rec conv_join = function\r
 325   | [] -> "@"\r
 326   | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
 327  print_hline ();\r
 328  let conv = conv_join convs in\r
 329  let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
 330  let varno = List.length var_names in\r
 331  let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
 332  (* initial sanity check *)\r
 333  sanity p\r
 334 ;;\r
 335 \r
 336 let solve p =\r
 337  if eta_subterm p.div p.conv\r
 338   then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
 339   else check p (auto p)\r
 340 ;;\r
 341 \r
 342 let run x y = solve (problem_of x y);;\r
 343 \r
 344 (* Example usage of interactive: *)\r
 345 \r
 346 (* let interactive div conv cmds =\r
 347  let p = problem_of div conv in\r
 348  try (\r
 349  let p = List.fold_left (|>) p cmds in\r
 350  let rec f p cmds =\r
 351   let nth spl n = int_of_string (List.nth spl n) in\r
 352   let read_cmd () =\r
 353    let s = read_line () in\r
 354    let spl = Str.split (Str.regexp " +") s in\r
 355    s, let uno = List.hd spl in\r
 356     try if uno = "eat" then eat\r
 357     else if uno = "step" then step (nth spl 1) (nth spl 2)\r
 358     else failwith "Wrong input."\r
 359     with Failure s -> print_endline s; (fun x -> x) in\r
 360   let str, cmd = read_cmd () in\r
 361   let cmds = (" " ^ str ^ ";")::cmds in\r
 362   try\r
 363    let p = cmd p in f p cmds\r
 364   with\r
 365   | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
 366  in f p []\r
 367  ) with Done _ -> ()\r
 368 ;; *)\r
 369 \r
 370 (* interactive "x y"\r
 371  "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
 372 ;; *)\r
 373 \r
 374 run "x x" ["x y"; "y y"; "y x"] ;;\r
 375 run "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
 376 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
 377 \r
 378 run "x (y. x y y)" ["x (y. x y x)"] ;;\r
 379 \r
 380 run "x a a a a" [\r
 381  "x b a a a";\r
 382  "x a b a a";\r
 383  "x a a b a";\r
 384  "x a a a b";\r
 385 ] ;;\r
 386 \r
 387 (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
 388 run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
 389  "x a a a a (_. a) b b b";\r
 390  "x a a a a (_. _. _. _. x. y. x y)";\r
 391 ] ;;\r
 392 \r
 393 (* bug in eat that was erasing terms in convergent that then diverged *)\r
 394 run "x y z"\r
 395 [\r
 396 "x @ @";\r
 397 "z (y @ (y @))"\r
 398 ] ;;\r
 399 \r
 400 (* bug in no_leading_lambdas where x in j-th position *)\r
 401 run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
 402 ["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
 403 ;;\r
 404 \r
 405 print_hline();\r
 406 print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r