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  | C _ as t -> t\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, t =\r
 251   match phase with\r
 252   | `One ->\r
 253       let n = 1 + max\r
 254        (compute_max_lambdas_at var k p.div)\r
 255        (compute_max_lambdas_at var k 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 p, A(t, delta)\r
 262   | `Two -> p, delta in\r
 263  let subst = var, mk_lams t k in\r
 264  let p = subst_in_problem subst p in\r
 265  sanity p;\r
 266  let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in\r
 267  sanity p\r
 268 ;;\r
 269 \r
 270 (* step on the head of div, on the k-th argument, with n fresh vars *)\r
 271 let step k n p =\r
 272  let var, _ = get_inert p.div in\r
 273 print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 274  let p, t = (* apply fresh vars *)\r
 275   fold_nat (fun (p, t) _ ->\r
 276     let p, v = freshvar p in\r
 277     p, A(t, V (v + k + 1))\r
 278   ) (p, V 0) n in\r
 279  let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
 280   fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
 281  let t = mk_lams t (k+1) in (* make leading lambdas *)\r
 282  let subst = var, t in\r
 283  let p = subst_in_problem subst p in\r
 284  sanity p\r
 285 ;;\r
 286 ;;\r
 287 \r
 288 let parse strs =\r
 289   let rec aux level = function\r
 290   | Parser_andrea.Lam t -> L (aux (level + 1) t)\r
 291   | Parser_andrea.App (t1, t2) ->\r
 292    if level = 0 then mk_app (aux level t1) (aux level t2)\r
 293     else A(aux level t1, aux level t2)\r
 294   | Parser_andrea.Var v -> V v in\r
 295   let (tms, free) = Parser_andrea.parse_many strs in\r
 296   (List.map (aux 0) tms, free)\r
 297 ;;\r
 298 \r
 299 let rec auto p =\r
 300  let hd_var, n_args = get_inert p.div in\r
 301  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
 302  | None ->\r
 303    (try\r
 304     let phase = p.phase in\r
 305      let p = eat p in\r
 306      if phase = `Two\r
 307       then problem_fail p "Auto.2 did not complete the problem"\r
 308       else auto p\r
 309     with Done sigma -> sigma)\r
 310  | Some t ->\r
 311   let j = find_eta_difference p t n_args - 1 in\r
 312   let k = 1 + max\r
 313    (compute_max_lambdas_at hd_var j p.div)\r
 314     (compute_max_lambdas_at hd_var j p.conv) in\r
 315   let p = step j k p in\r
 316   auto p\r
 317 ;;\r
 318 \r
 319 let problem_of div convs =\r
 320  let rec conv_join = function\r
 321   | [] -> "@"\r
 322   | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
 323  print_hline ();\r
 324  let conv = conv_join convs in\r
 325  let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
 326  let varno = List.length var_names in\r
 327  let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
 328  (* initial sanity check *)\r
 329  sanity p\r
 330 ;;\r
 331 \r
 332 let solve p =\r
 333  if eta_subterm p.div p.conv\r
 334   then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
 335   else check p (auto p)\r
 336 ;;\r
 337 \r
 338 let run x y = solve (problem_of x y);;\r
 339 \r
 340 (* Example usage of interactive: *)\r
 341 \r
 342 (* let interactive div conv cmds =\r
 343  let p = problem_of div conv in\r
 344  try (\r
 345  let p = List.fold_left (|>) p cmds in\r
 346  let rec f p cmds =\r
 347   let nth spl n = int_of_string (List.nth spl n) in\r
 348   let read_cmd () =\r
 349    let s = read_line () in\r
 350    let spl = Str.split (Str.regexp " +") s in\r
 351    s, let uno = List.hd spl in\r
 352     try if uno = "eat" then eat\r
 353     else if uno = "step" then step (nth spl 1) (nth spl 2)\r
 354     else failwith "Wrong input."\r
 355     with Failure s -> print_endline s; (fun x -> x) in\r
 356   let str, cmd = read_cmd () in\r
 357   let cmds = (" " ^ str ^ ";")::cmds in\r
 358   try\r
 359    let p = cmd p in f p cmds\r
 360   with\r
 361   | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
 362  in f p []\r
 363  ) with Done _ -> ()\r
 364 ;; *)\r
 365 \r
 366 (* interactive "x y"\r
 367  "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
 368 ;; *)\r
 369 \r
 370 run "x x" ["x y"; "y y"; "y x"] ;;\r
 371 run "x y" ["x (_. x)"; "y z"; "y x"] ;;\r
 372 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
 373 \r
 374 run "x (y. x y y)" ["x (y. x y x)"] ;;\r
 375 \r
 376 run "x a a a a" [\r
 377  "x b a a a";\r
 378  "x a b a a";\r
 379  "x a a b a";\r
 380  "x a a a b";\r
 381 ] ;;\r
 382 \r
 383 (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
 384 run "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [\r
 385  "x a a a a (_. a) b b b";\r
 386  "x a a a a (_. _. _. _. x. y. x y)";\r
 387 ] ;;\r
 388 \r
 389 (* bug in no_leading_lambdas where x in j-th position *)\r
 390 run "v0 (v1 v2) (x. y. v0 v3 v4 v2)"\r
 391 ["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
 392 ;;\r
 393 \r
 394 print_hline();\r
 395 print_endline ">>> EXAMPLES IN simple.ml FINISHED <<<"\r