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