ocaml/andrea8.ml

   1 let (++) f g x = f (g x);;\r
   2 \r
   3 let print_hline = Console.print_hline;;\r
   4 \r
   5 type var = int;;\r
   6 type t =\r
   7  | V of var\r
   8  | A of t * t\r
   9  | L of t\r
  10  | B (* bottom *)\r
  11  | P (* pacman *)\r
  12  (* | Stuck of var * int *)\r
  13  (* | Ptr of int *)\r
  14 ;;\r
  15 \r
  16 let rec consts = (* const_apps, const_lambda *)\r
  17  let rec aux1 = function\r
  18  | A(t, _) -> 1 + aux1 t\r
  19  | _ -> 0 in\r
  20  let rec aux2 = function\r
  21  | L t -> 1 + aux2 t\r
  22  | _ -> 0 in\r
  23  function\r
  24  | A(t1, t2) as t ->\r
  25     let a1, b1 = consts t1 in\r
  26     let a2, b2 = consts t2 in\r
  27     max (aux1 t) (max a1 a2), max b1 b2\r
  28  | L t' as t ->\r
  29     let a, b = consts t' in\r
  30     a, max (aux2 t) b\r
  31  | _ -> 0, 0\r
  32 ;;\r
  33 \r
  34 \r
  35 type problem = {\r
  36    orig_freshno: int\r
  37  ; freshno : int\r
  38  ; div : t\r
  39  ; conv : t list\r
  40  ; matches : (var (* variable originating this match *) * ((bool (* coming from div *) * t (* term to discriminate *) * var (* continuation *))) list) list\r
  41  ; sigma : (var * t) list (* substitutions *)\r
  42  ; stepped : var list\r
  43  ; arities : (var * int) list\r
  44  ; k_app : int\r
  45  ; k_lam : int\r
  46 }\r
  47 \r
  48 let dummy_p = {orig_freshno=0; freshno=0; div=B; conv=[]; matches=[]; sigma=[]; stepped=[]; arities=[]; k_app=0;k_lam=0};;\r
  49 \r
  50 let append_conv p t = let len = List.length p.conv in let p = {p with conv=t::p.conv} in p, len;;\r
  51 let get_conv p n = List.nth p.conv (List.length p.conv - 1 - n);;\r
  52 let index_of_conv t conv = List.length conv - 1 - (Util.index_of t conv);;\r
  53 \r
  54 let eq_conv = (=);;\r
  55 let eq_conv_indices p i j = eq_conv (get_conv p i) (get_conv p j);;\r
  56 let all_terms p = (p.div :: p.conv) @ Util.concat_map (fun (_, lst) -> List.map (fun (_,x,_) -> x) lst) p.matches;;\r
  57 \r
  58 exception Done of (var * t) list (* substitution *);;\r
  59 exception Fail of int * string;;\r
  60 \r
  61 let string_of_t p =\r
  62   let bound_vars = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"; "x3"; "x4"; "x5"] in\r
  63   let rec string_of_term_w_pars level = function\r
  64     | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)\r
  65     | A _\r
  66     | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"\r
  67     | B -> "BOT"\r
  68     | P -> "PAC"\r
  69     (* | Stuck _ as t -> "(" ^ string_of_term_no_pars_app level t ^ ")" *)\r
  70     (* | Ptr _ as t-> "(" ^ string_of_term_no_pars_app level t ^ ")" *)\r
  71     (* "&" ^ string_of_int n *)\r
  72   and string_of_term_no_pars_app level = function\r
  73     | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)\r
  74     (* | Stuck(v,n) -> ":" ^ string_of_term_no_pars_app level (V v) ^ " " ^ (string_of_term_w_pars level (get_conv p n)) *)\r
  75     (* | Ptr n -> string_of_term_no_pars_app level (get_conv p n) *)\r
  76     (* | Ptr n -> "&" ^ string_of_int n *)\r
  77     | _ as t -> string_of_term_w_pars level t\r
  78   and string_of_term_no_pars_lam level = function\r
  79     | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)\r
  80     | _ as t -> string_of_term_no_pars level t\r
  81   and string_of_term_no_pars level = function\r
  82     | L _ as t -> string_of_term_no_pars_lam level t\r
  83     | _ as t -> string_of_term_no_pars_app level t\r
  84   in string_of_term_no_pars 0\r
  85 ;;\r
  86 \r
  87 let string_of_problem p =\r
  88  let lines = [\r
  89   "[arities] " ^ String.concat " " (List.map (fun (v,n) -> "`" ^ string_of_int v ^ "=" ^ string_of_int n) p.arities);\r
  90   "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);\r
  91   "[DV] " ^ (string_of_t p p.div);\r
  92   "[CV] " ^ String.concat "\n     " (List.map (string_of_t p) p.conv);\r
  93   (* "" ; *)\r
  94  ] @ Util.concat_map (fun (v, lst) -> ("[<>] of "^(string_of_t p (V v))) :: List.map (fun (b,t,c) -> (if b then " * " else "   ") ^ string_of_t p t\r
  95  ^ " -> " ^ string_of_t p (V c)\r
  96  ) lst) p.matches @ [""] in\r
  97  String.concat "\n" lines\r
  98 ;;\r
  99 \r
 100 let problem_fail p reason =\r
 101  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
 102  print_endline (string_of_problem p);\r
 103  raise (Fail (-1, reason))\r
 104 ;;\r
 105 \r
 106 let freshvar ({freshno} as p) =\r
 107  {p with freshno=freshno+1}, freshno+1\r
 108 ;;\r
 109 \r
 110 let add_to_match p id fromdiv t =\r
 111  let p, v = freshvar p in\r
 112  let arity = (List.assoc id p.arities) - 1 in\r
 113  let entry = fromdiv, t, v in\r
 114  let matches =\r
 115   List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry::lst)) p.matches\r
 116   in\r
 117  let arities = (v,arity) :: p.arities in\r
 118  {p with matches; arities}, V v\r
 119 ;;\r
 120 \r
 121 let var_occurs_in p v =\r
 122  let rec aux level = function\r
 123  | V v' -> v + level = v'\r
 124  (* | Stuck(v',n) -> assert (v <> v'); aux level (get_conv p n) *)\r
 125  | A(t1,t2) -> (aux level t1) || (aux level t2)\r
 126  | L t -> aux (level+1) t\r
 127  | B -> false\r
 128  | P -> false\r
 129  (* | Ptr n -> aux level (get_conv p n) *)\r
 130 \r
 131  in aux 0\r
 132 ;;\r
 133 \r
 134 let rec is_inert p =\r
 135  function\r
 136  | A(t,_) -> is_inert p t\r
 137  (* | Ptr n -> is_inert p (get_conv p n) *)\r
 138  | V _ -> true\r
 139  | L _ | B | P -> false\r
 140 ;;\r
 141 \r
 142 let is_var = function V _ -> true | _ -> false;;\r
 143 let is_lambda = function L _ -> true | _ -> false;;\r
 144 let is_pacman = function P -> true | _ -> false;;\r
 145 \r
 146 let rec subst level delift fromdiv sub p =\r
 147  function\r
 148  | V v -> p, if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
 149  | L t -> let p, t = subst (level + 1) delift fromdiv sub p t in p, L t\r
 150  | A (t1,t2) ->\r
 151   let p, t1 = subst level delift fromdiv sub p t1 in\r
 152   let p, t2 = subst level delift fromdiv sub p t2 in\r
 153   if t1 = B || t2 = B then p, B else\r
 154   if level = 0 then mk_app fromdiv p t1 t2 else p, A (t1, t2)\r
 155  | B -> p, B\r
 156  | P -> p, P\r
 157 and mk_app fromdiv p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
 158  | B | _ when t2 = B -> p, B\r
 159  | L t1 -> subst 0 true fromdiv (0, t2) p t1\r
 160  | V v when List.mem v p.stepped ->\r
 161     let p, x = add_to_match p v fromdiv t2 in\r
 162     p, x\r
 163  | t1 -> p, A (t1, t2)\r
 164 and mk_apps fromdiv p t =\r
 165  function\r
 166  | [] -> p, t\r
 167  | t'::ts -> let p, t = mk_app fromdiv p t t' in mk_apps fromdiv p t ts\r
 168 and lift n =\r
 169  let rec aux n' =\r
 170   function\r
 171   | V m -> V (if m >= n' then m + n else m)\r
 172   | L t -> L (aux (n'+1) t)\r
 173   | A (t1, t2) -> A (aux n' t1, aux n' t2)\r
 174   | B -> B\r
 175   | P -> P\r
 176  in aux 0\r
 177 ;;\r
 178 \r
 179 let subst = subst 0 false;;\r
 180 \r
 181 let mk_lambda t = L (lift 1 t) ;;\r
 182 \r
 183 let subst_conv sub =\r
 184  let rec aux p = function\r
 185  | [] -> p, []\r
 186  | t::tms ->\r
 187   let p, tms = aux p tms in\r
 188   let p, t = subst false sub p t in\r
 189   p, t :: tms\r
 190  in aux\r
 191 ;;\r
 192 \r
 193 let subst_in_problem (sub: var * t) (p: problem) =\r
 194 print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
 195 (* BUG QUI FIXME!!!! *)\r
 196  let rec mix l1 l2 = match l1, l2 with\r
 197  | [], l2 -> l2\r
 198  | x::xs, _::ys -> x:: (mix xs ys)\r
 199  | _ -> assert false in\r
 200  let p = {p with stepped=(fst sub)::p.stepped} in\r
 201  let p, conv = subst_conv sub p p.conv in\r
 202  let p, div = subst true sub p p.div in\r
 203  let conv = List.rev (mix (List.rev conv) (List.rev p.conv)) in\r
 204  let p = {p with div; conv} in\r
 205  (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
 206  {p with sigma=sub::p.sigma}\r
 207 ;;\r
 208 \r
 209 (* FIXME *)\r
 210 let unify_terms p v1 v2 =\r
 211  if List.mem v1 p.stepped\r
 212   then problem_fail p "The collapse of a match came after too many steps :(";\r
 213  subst_in_problem (v1, V v2) p\r
 214 ;;\r
 215 \r
 216 let rec unify p =\r
 217  let rec give_duplicates =\r
 218   let rec aux' t = function\r
 219   | [] -> [], None\r
 220   | (b',t',c')::ts -> if t = t' (* FIXME! eta-eq here *) then ts, Some (b',c') else (\r
 221    let ts, res = aux' t ts in (b',t',c')::ts, res) in\r
 222   let rec aux = function\r
 223    | [] -> [], None\r
 224    | (b,t,c)::rest -> (\r
 225     match aux' t rest with\r
 226     | rest, None -> aux rest\r
 227     | rest, Some(b',c') -> (b || b', t, c) :: rest, Some(c', c)\r
 228     ) in\r
 229   function\r
 230   | [] -> [], None\r
 231   | (orig,branches) :: ms ->\r
 232    match aux branches with\r
 233    | _, None -> let ms, res = give_duplicates ms in (orig,branches) :: ms, res\r
 234    | branches', Some subst -> (orig,branches') :: ms, Some subst in\r
 235  let matches, vars_to_be_unified = give_duplicates p.matches in\r
 236  let p = {p with matches=matches} in\r
 237  match vars_to_be_unified with\r
 238   | None -> p\r
 239   | Some(t', t) ->\r
 240    (* print_endline ("> unify " ^ string_of_t p (t') ^ " with " ^ string_of_t p t); *)\r
 241    unify (unify_terms p t' t)\r
 242 ;;\r
 243 \r
 244 let problem_done p =\r
 245  let condition (b, t, cont) =\r
 246   (b && t = B) ||\r
 247   (not (List.mem cont p.stepped)) ||\r
 248   is_var t in\r
 249  let all_separated = List.for_all (fun (_, lst) -> List.for_all condition lst) p.matches in\r
 250  all_separated && p.div = B\r
 251 ;;\r
 252 \r
 253 let free_vars p t =\r
 254  let rec aux level = function\r
 255  | V v -> if v >= level then [v] else []\r
 256  | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
 257  | L t -> aux (level+1) t\r
 258  | B | P -> []\r
 259  in Util.sort_uniq (aux 0 t)\r
 260 ;;\r
 261 \r
 262 let visible_vars p t =\r
 263  let rec aux = function\r
 264  | V v -> [v]\r
 265  | A(t1,t2) -> (aux t1) @ (aux t2)\r
 266  | B | P\r
 267  | L _ -> []\r
 268  (* | Ptr n -> aux (get_conv p n) *)\r
 269  in Util.sort_uniq (aux t)\r
 270 ;;\r
 271 \r
 272 \r
 273 let rec simple_explode p =\r
 274  match p.div with\r
 275  | V var ->\r
 276   let subst = var, B in\r
 277   sanity (subst_in_problem subst p)\r
 278  | _ -> p\r
 279 \r
 280 and sanity p =\r
 281  (* Sanity checks: *)\r
 282  if (function | P | L _ -> true | _ -> false) p.div then problem_fail p "p.div converged";\r
 283  if List.mem B p.conv then problem_fail p "p.conv diverged";\r
 284  let solvable (b,t,c) = (b && not (List.mem c p.stepped)) || is_inert p t in\r
 285  if not (List.for_all (fun (_, lst) -> List.for_all solvable lst) p.matches)\r
 286   then problem_fail p "Unsolvable discrimination";\r
 287 \r
 288  let p = unify p in\r
 289  print_endline (string_of_problem p); (* non cancellare *)\r
 290  let p = if problem_done p then raise (Done p.sigma) else p in\r
 291  let p = if is_var p.div then simple_explode p else p in\r
 292  p\r
 293 ;;\r
 294 \r
 295 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 296 \r
 297 let rec hd_args t = match t with\r
 298  | V v -> v, []\r
 299  | A(t1,t2) -> let a, b = hd_args t1 in a, b @ [t2]\r
 300  | _ -> -666, []\r
 301 ;;\r
 302 \r
 303 let max_arity_of_var v =\r
 304  let rec aux level =\r
 305  function\r
 306  | V _ -> 0\r
 307  | A _ as t -> print_string (string_of_t dummy_p t); let hd, args = hd_args t in\r
 308     let acc = if hd = level + v then List.length args else 0 in\r
 309     List.fold_right (max ++ (aux level)) args acc\r
 310  | L t -> aux (level + 1) t\r
 311  | P | B -> 0\r
 312  in aux 0\r
 313 ;;\r
 314 \r
 315 let ignore var n p =\r
 316  print_cmd "EAT" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 317  let rec aux m t =\r
 318   if m = 0\r
 319    then lift n t\r
 320    else L (aux (m-1) t) in\r
 321  let p, fresh = freshvar p in\r
 322  let subst = var, aux n (V fresh) in\r
 323  sanity (subst_in_problem subst p)\r
 324 ;;\r
 325 \r
 326 \r
 327 \r
 328 let eat var p =\r
 329  print_cmd "EAT" ("var " ^ string_of_t p (V var));\r
 330  let rec is_hd v' = function\r
 331  | A (t,_) -> is_hd v' t\r
 332  | V v -> v' = v\r
 333  | _ -> false in\r
 334  let rec app_length = function\r
 335  | A (t,_) -> 1 + app_length t\r
 336  | _ -> 0 in\r
 337  let rec find_app_no = function\r
 338  | V _ | L _ | P | B -> 0\r
 339  | A (t1,t2) as t ->\r
 340     max (max (find_app_no t1) (find_app_no t2))\r
 341      (if is_hd var t1 then app_length t else 0)\r
 342  in let n = List.fold_right (max ++ find_app_no) (all_terms p) 0 in\r
 343  let rec aux m t =\r
 344   if m = 0\r
 345    then lift n t\r
 346    else L (aux (m-1) t) in\r
 347  let p, fresh = freshvar p in\r
 348  let subst = var, aux n (V fresh) in\r
 349  sanity (subst_in_problem subst p)\r
 350 ;;\r
 351 \r
 352 (* let explode p =\r
 353  let fv1 = visible_vars p p.div in\r
 354  let fv2 = List.concat (List.map (visible_vars p) p.conv) in\r
 355  let fv = List.filter (fun x -> not (List.mem x fv2)) fv1 in\r
 356  let fv = List.filter ((<) p.orig_freshno) fv in\r
 357  match fv with\r
 358  | var::_ ->\r
 359   print_cmd "EXPLODE" ("on " ^ string_of_t p (V var));\r
 360   let subst = var, B in\r
 361   sanity (subst_in_problem subst p)\r
 362  | _ -> raise (Fail (-1,"premature explosion"))\r
 363 ;; *)\r
 364 \r
 365 (* let step var p =
 366  print_cmd "STEP" ("on " ^ string_of_t p (V var));
 367  let matches = (var,[])::p.matches in
 368  let p = {p with matches;stepped=var::p.stepped} in
 369  let subst = var, V var in
 370  sanity (subst_in_problem subst p)\r
 371 ;; *)\r
 372 \r
 373 let choose n p =\r
 374  print_cmd "CHOOSE" ("#" ^ string_of_int n);\r
 375  let rec aux n t = match t with\r
 376  | V _ -> 0, t\r
 377  | A(t1,_) -> let n', t' = aux n t1 in if n = n' then n', t' else n'+1, t\r
 378  | _ -> assert false\r
 379  in let n', div = aux n p.div in\r
 380  if n' <> n then problem_fail p "wrong choose";\r
 381  let p = {p with div} in\r
 382  sanity p\r
 383 ;;\r
 384 \r
 385 let apply var appk p =\r
 386  print_cmd "APPLY"\r
 387   (string_of_t p (V var) ^ " applies no." ^ string_of_int appk ^ " fresh variables");\r
 388  let rec mk_freshvars n p =\r
 389   if n = 0\r
 390    then p, []\r
 391    else\r
 392     let p, vs = mk_freshvars (n-1) p in\r
 393     let p, v = freshvar p in\r
 394     p, V(v)::vs in\r
 395  let p, vars = mk_freshvars appk p in\r
 396  let p, t = mk_apps false p (V 0) (List.map (lift 1) vars) in\r
 397  let t = L (A (lift 1 (V var), t))  in\r
 398  let subst = var, t in\r
 399  sanity (subst_in_problem subst p)\r
 400 ;;\r
 401 \r
 402 let find_arities_after_app p =\r
 403  let rec aux level n = function\r
 404  | L t -> assert (n > 0); max_arity_of_var level t :: aux (level+1) (n-1) t\r
 405  | _ -> Array.to_list (Array.make n 0)\r
 406  in aux 0\r
 407 ;;\r
 408 let find_all_first_args_of v =\r
 409  let rec aux level = function\r
 410  | L t -> aux (level+1) t\r
 411  | V _ -> []\r
 412  | A(V v', t2) -> (if v + level = v' then [t2] else []) @ aux level t2\r
 413  | A(t1,t2) -> aux level t1 @ aux level t2\r
 414  | _ -> []\r
 415  in aux 0\r
 416 ;;\r
 417 \r
 418 let step' var p =\r
 419  let appk = p.k_lam + p.k_app + 1 in\r
 420  print_cmd "STEP'" ("on " ^ string_of_t p (V var) ^ " and applies no." ^ string_of_int appk ^ " fresh variables");\r
 421  let p, vars = (* +1 below because of lifting *)\r
 422   Array.fold_left (fun (p,vars) _ -> let p, v = freshvar p in p, (v+1)::vars)\r
 423    (p, []) (Array.make appk ()) in\r
 424  let p, t = mk_apps false p (V 0) (List.map (fun x -> V x) vars) in\r
 425 \r
 426  let first_args = Util.sort_uniq (List.fold_right ((@) ++ (find_all_first_args_of var)) (all_terms p) []) in\r
 427  let map = List.fold_left (fun acc t -> let acc' = find_arities_after_app p appk t in List.map (fun (x,y) -> max x y) (List.combine acc acc')) (Array.to_list (Array.make appk 0)) first_args in\r
 428  let arities = List.combine (List.map ((+) (-1)) vars) map in\r
 429 \r
 430  (* let p, var' = freshvar p in *)\r
 431  let p, var' = p, var in\r
 432  let matches = (var', []) :: p.matches in\r
 433  let p = {p with matches; arities=arities@p.arities} in\r
 434  let t = L (A (lift 1 (V var'), t))  in\r
 435  let subst = var, t in\r
 436  sanity (subst_in_problem subst p)\r
 437 ;;\r
 438 \r
 439 let perm var n p =\r
 440  if n = 1 then p else (\r
 441  print_cmd "PERM" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 442  (* let p, v = freshvar p in *)\r
 443  let p, v = p, var in\r
 444  let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in\r
 445  let rec aux m t =\r
 446   if m = 0\r
 447    then aux' (n-1) t\r
 448    else L (aux (m-1) t) in\r
 449  let t = aux n (lift n (V v)) in\r
 450  let subst = var, t in\r
 451  (* let p = {p with arities=(v, List.assoc var p.arities)::p.arities} in *)\r
 452  sanity (subst_in_problem subst p)\r
 453 ) ;;\r
 454 \r
 455 let free_vars_of_p p =\r
 456  Util.sort_uniq (Util.concat_map (free_vars p) (all_terms p));;\r
 457 \r
 458 let rec applied_vars p = function\r
 459 | B | P -> []\r
 460 | L _ -> [] (* ??? *)\r
 461 | V _ -> []\r
 462 | A(V v,t2) -> v :: applied_vars p t2\r
 463 | A(t1,t2) -> applied_vars p t1 @ applied_vars p t2\r
 464 ;;\r
 465 \r
 466 let applied_vars_of_p p =\r
 467  Util.sort_uniq (Util.concat_map (applied_vars p) (all_terms p));;\r
 468 \r
 469 let rec auto p =\r
 470  let aux f var =\r
 471   try\r
 472    auto (f var); ()\r
 473   with\r
 474   (* | Done _ as d -> raise d *)\r
 475   | Fail(_, s) -> print_endline ("<<< Backtracking because: " ^ s) in\r
 476  print_endline ">>> auto called";\r
 477  (* Compute useful free variables *)\r
 478  let fv = applied_vars_of_p p in\r
 479  let fv = List.filter (fun v -> not (List.mem v p.stepped)) fv in\r
 480  List.iter (fun v -> print_string ("@`" ^ string_of_int v)) fv;\r
 481  let fv0 = List.filter (fun v -> List.assoc v p.arities > 0) fv in (* remove variable with arity left 0, cannot step there *)\r
 482  if fv0 = [] then (print_endline "warning! empty step fv0"; List.iter (fun v -> print_string ("@`" ^ string_of_int v)) fv);\r
 483  let permute_and_step p v =\r
 484   let step'' problem prm var =\r
 485    let problem = perm var prm problem in\r
 486    (* let _ = read_line () in *)\r
 487    let problem = step' var problem in\r
 488    problem in\r
 489   let arity = List.assoc v p.arities in\r
 490   let _, perms = Array.fold_left (fun (arity, acc) () -> let a = arity + 1 in a, a::acc) (1,[1]) (Array.make (arity-1) ()) in\r
 491   List.iter (fun perm -> aux (step'' p perm) v) perms\r
 492  in\r
 493  List.iter (permute_and_step p) fv0;\r
 494  List.iter (aux (fun v -> eat v p)) fv;\r
 495  (* mancano: applicazioni e choose; ??? *)\r
 496 ;;\r
 497 \r
 498 let parse strs =\r
 499   let rec aux level = function\r
 500   | Parser.Lam t -> L (aux (level + 1) t)\r
 501   | Parser.App (t1, t2) ->\r
 502    if level = 0 then snd (mk_app false dummy_p (aux level t1) (aux level t2))\r
 503     else A(aux level t1, aux level t2)\r
 504   | Parser.Var v -> V v\r
 505   in let (tms, free) = Parser.parse_many strs\r
 506   in (List.map (aux 0) tms, free)\r
 507 ;;\r
 508 \r
 509 let magic6 div conv cmds =\r
 510  print_hline ();\r
 511  let all_tms, var_names = parse (div :: conv) in\r
 512  let div, conv = List.hd all_tms, List.tl all_tms in\r
 513  let varno = List.length var_names in\r
 514  let k_app, k_lam = List.fold_left (fun (a, b) t -> let a', b' = consts t in max a a', max b b') (0,0) all_tms in\r
 515  let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]; stepped=[];k_app;k_lam;arities=[]} in\r
 516  let fv = Util.sort_uniq (Util.concat_map (free_vars p) all_tms) in\r
 517  let arities = List.map (fun var -> var, k_app) fv in\r
 518  let p = {p with arities} in\r
 519  let p = try\r
 520   let subst = Util.index_of "BOMB" var_names, L B in\r
 521   let p = subst_in_problem subst p in p\r
 522   with Not_found -> p in\r
 523  let p = sanity p in\r
 524  try\r
 525   problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
 526  with\r
 527  | Done _ -> ()\r
 528 ;;\r
 529 \r
 530 let auto div conv =\r
 531  print_hline ();\r
 532  let all_tms, var_names = parse (div :: conv) in\r
 533  let div, conv = List.hd all_tms, List.tl all_tms in\r
 534  let varno = List.length var_names in\r
 535  let k_app, k_lam = List.fold_left (fun (a, b) t -> let a', b' = consts t in max a a', max b b') (0,0) all_tms in\r
 536  let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]; stepped=[];k_app;k_lam;arities=[]} in\r
 537  let fv = Util.sort_uniq (Util.concat_map (free_vars p) all_tms) in\r
 538  let max_arity_of_var_in_p var p =\r
 539   1 + List.fold_right (max ++ (max_arity_of_var var)) (all_terms p) 0 in\r
 540  let arities = List.map (fun var -> var, max_arity_of_var_in_p var p) fv in\r
 541  let p = {p with arities} in\r
 542  let p = try\r
 543   let subst = Util.index_of "BOMB" var_names, L B in\r
 544   let p = subst_in_problem subst p in p\r
 545   with Not_found -> p in\r
 546  let p = sanity p in\r
 547  try\r
 548   auto p;\r
 549   failwith "auto failed."\r
 550  with\r
 551  | Done _ -> print_endline "<<< auto ok >>>"; (* TODO: print and verify substitution *)\r
 552 ;;\r
 553 \r
 554 (* let interactive div conv cmds =\r
 555  print_hline ();\r
 556  let all_tms, var_names = parse (div @ conv) in\r
 557  let div, conv = list_split (List.length div) all_tms in\r
 558  let varno = List.length var_names in\r
 559  let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in\r
 560  (* activate bombs *)\r
 561  let p = try\r
 562   let subst = Util.index_of "BOMB" var_names, L B in\r
 563    subst_in_problem subst p\r
 564   with Not_found -> p in\r
 565  (* activate pacmans *)\r
 566  let p = try\r
 567   let subst = Util.index_of "PACMAN" var_names, P in\r
 568    let p = subst_in_problem subst p in\r
 569    (print_endline ("after subst in problem " ^ string_of_problem p); p)\r
 570   with Not_found -> p in\r
 571  (* initial sanity check *)\r
 572  let p = sanity p in\r
 573  let p = List.fold_left (|>) p cmds in\r
 574  let rec f p cmds =\r
 575   let nth spl n = int_of_string (List.nth spl n) in\r
 576   let read_cmd () =\r
 577    let s = read_line () in\r
 578    let spl = Str.split (Str.regexp " +") s in\r
 579    s, let uno = List.hd spl in\r
 580     try if uno = "explode" then explode\r
 581     else if uno = "ignore" then ignore (nth spl 1) (nth spl 2)\r
 582     else if uno = "step" then step (nth spl 1)\r
 583     else if uno = "perm" then perm (nth spl 1) (nth spl 2)\r
 584     else if uno = "apply" then apply (nth spl 1) (nth spl 2)\r
 585     (* else if uno = "forget" then forget (nth spl 1) (nth spl 2) *)\r
 586     else if uno = "id" then id (nth spl 1)\r
 587     else failwith "Wrong input."\r
 588     with Failure s -> print_endline s; (fun x -> x) in\r
 589   let str, cmd = read_cmd () in\r
 590   let cmds = (" " ^ str ^ ";")::cmds in\r
 591   try\r
 592    let p = cmd p in f p cmds\r
 593   with\r
 594   | Done -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
 595  in f p []\r
 596 ;; *)\r
 597 \r
 598 let _ = auto\r
 599  "x x"\r
 600  [ "_. BOMB" ]\r
 601  (* [ eat 1 ] *)\r
 602 ;;\r
 603 \r
 604 \r
 605 let _ = auto\r
 606    "x y BOMB b"\r
 607  [ "x BOMB y c" ]\r
 608  (* [ perm 1 3; step' 8 ; eat 4; eat 5; eat 15; ] *)\r
 609 ;;\r
 610 \r
 611 \r
 612 let _ = auto\r
 613  "x BOMB a1 c"\r
 614  [ "x y BOMB d"; "x BOMB a2 c" ]\r
 615  (* [ perm 1 3 ; step' 10 ; eat 4; eat 6;  step' 17; eat 3; eat 7; eat 27; ] *)\r
 616 ;;\r
 617 \r
 618 \r
 619 let _ = auto\r
 620  "x (x x)"\r
 621  [ "x x" ; "x x x" ]\r
 622  (* [\r
 623  step' 1;\r
 624  eat 6; eat 9; eat 13;\r
 625 ]*)\r
 626 ;;\r
 627 \r
 628 \r
 629 (* let _ = auto\r
 630  "x (_.BOMB)"\r
 631  [ "x (_._. BOMB)" ]\r
 632  (* [ apply 1 2; ] *)\r
 633 ;; *)\r
 634 \r
 635 \r
 636 let _ = auto\r
 637  "x (_.y)"\r
 638  [ "y (_. x)" ]\r
 639  (* [ apply 1 1; ignore 1 1;  explode; ] *)\r
 640 ;;\r
 641 \r
 642 \r
 643 let _ = auto\r
 644  "y (x a1 BOMB c) (x BOMB b1 d)"\r
 645  [ "y (x a2 BOMB c) (x BOMB b1 d)";\r
 646  "y (x a1 BOMB c) (x BOMB b2 d)";]\r
 647  (* [perm 2 3;\r
 648  step 12;\r
 649  perm 17 2;\r
 650  step 19;\r
 651  step 18;\r
 652  ignore 22 1;\r
 653  ignore 21 1;\r
 654  ignore 24 1;\r
 655  ignore 25 1;\r
 656  step 1;\r
 657  step 32;\r
 658  explode;\r
 659  ] *)\r
 660 ;;\r
 661 \r
 662 let _ = auto\r
 663 "PACMAN (x x x)" ["PACMAN (x x)"];;\r
 664 \r
 665 (*\r
 666 let _ = magic6\r
 667  ["z (y x)"]\r
 668  [ "z (y (x.x))"; "y (_. BOMB)" ]\r
 669  [ apply 2 1; step 3; explode; ]\r
 670 ;;\r
 671 \r
 672 let _ = magic6\r
 673  ["y x"]\r
 674  [ "y (x.x)"; "x (_. BOMB)" ]\r
 675  [ apply 1 1; ignore 2 1; step 1; explode; ]\r
 676 ;;\r
 677 \r
 678 let _ = magic6\r
 679  ["z (y x)"]\r
 680  [ "z (y (x.x))"; "y (_. BOMB)" ]\r
 681  [ step 1; explode; apply 2 1; id 2; ignore 3 1; ]\r
 682 ;;\r
 683 \r
 684 let _ = magic6\r
 685  ["y (x a)"]\r
 686  [ "y (x b)"; "x BOMB" ] [\r
 687  id 2;\r
 688  step 1;\r
 689  explode;\r
 690 ];;\r
 691 \r
 692 magic6\r
 693  ["y (x a)"] [ "y (x b)"; "x BOMB"; "y a" ]\r
 694  [\r
 695  apply 1 1;\r
 696  perm 2 2;\r
 697  ignore 9 1;\r
 698  step 10;\r
 699  explode;\r
 700  ];;\r
 701 (* "y (a c)"\r
 702 [ "y (b c)"; "y (x a)"; "y (x b)"; "x BOMB" ]  *)\r
 703 \r
 704 magic6\r
 705 ["x a (x (a.y BOMB))"]\r
 706 [ "x b"; "x (y c)"; "x (y d)" ]\r
 707 [apply 1 1;\r
 708 apply 2 1;\r
 709 explode;]\r
 710 (* [\r
 711 step 1;\r
 712 step 3;\r
 713 explode' 10;\r
 714 (* ma si puo' fare anche senza forget *) *)\r
 715 (* ] *)\r
 716 ;;\r
 717 \r
 718 (* dipendente dalla codifica? no, ma si risolve solo con id *)\r
 719 magic6\r
 720  ["y a"] ["y b"; "x (y (_.BOMB))"]\r
 721 [\r
 722 apply 1 1;\r
 723 apply 2 1;\r
 724 explode;\r
 725 ];;\r
 726  (* [id 1; explode];; *)\r
 727 \r
 728 magic6\r
 729  ["PACMAN (x x x)"] ["PACMAN (x x)"]\r
 730  [\r
 731  ignore 2 2;\r
 732  explode;\r
 733  ];; *)\r
 734 \r
 735 print_hline();\r
 736 print_endline "ALL DONE. "\r