ocaml/andrea6.ml

   1 let print_hline = Console.print_hline;;\r
   2 \r
   3 type var = int;;\r
   4 \r
   5 type t =\r
   6  | V of var\r
   7  | A of t * t\r
   8  | L of t\r
   9  | LM of\r
  10     t list (* body of the match *)\r
  11   * int (* explicit liftno *)\r
  12   * int (* variable which originated this match (id) *)\r
  13  | B (* bottom *)\r
  14  | P (* pacman *)\r
  15 ;;\r
  16 \r
  17 \r
  18 type problem = {\r
  19    freshno : int\r
  20  ; div : t\r
  21  ; conv : t list\r
  22  ; matches : (var (* variable originating this match *) * (t (* term to discriminate *) * t (* continuation *)) list) list\r
  23  ; sigma : (var * t) list (* substitutions *)\r
  24 }\r
  25 \r
  26 let string_of_t p =\r
  27  let bound_vars = ["x"; "y"; "z"; "z1"; "z2"] in\r
  28  let rec aux level = function\r
  29  | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)\r
  30  | A (t1,t2) -> "("^aux level t1^" "^aux level t2^")"\r
  31  | L t -> "(\\" ^ aux (level+1) (V 0) ^ ". " ^ aux (level+1) t ^ ")"\r
  32  | LM (ts,liftno,id) -> "[match orig="^aux 0 (V id)^"]"\r
  33  | B -> "BOT"\r
  34  | P -> "PAC"\r
  35  in aux 0\r
  36 ;;\r
  37 \r
  38 let string_of_problem p =\r
  39  let lines = [\r
  40   "[DV] " ^ string_of_t p p.div;\r
  41   "[CV] " ^ String.concat "\n     " (List.map (string_of_t p) p.conv);\r
  42   "" ;\r
  43  ] @ Util.concat_map (fun (_, lst) -> "[<>]" :: List.map (fun (t,c) -> "     " ^ string_of_t p t\r
  44  (* ^" -> " ^ string_of_t p c *)\r
  45  ) lst) p.matches @ [""] in\r
  46  String.concat "\n" lines\r
  47 ;;\r
  48 \r
  49 let problem_fail p reason =\r
  50  print_endline " FAIL FAIL FAIL FAIL FAIL FAIL FAIL FAIL FAIL";\r
  51  print_endline (string_of_problem p);\r
  52  failwith reason\r
  53 ;;\r
  54 \r
  55 let freshvar ({freshno} as p) =\r
  56  {p with freshno=freshno+1}, freshno+1\r
  57 ;;\r
  58 \r
  59 let add_to_match p id entry =\r
  60  let matches = try\r
  61    let _ = List.assoc id p.matches in\r
  62    List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry::lst) ) p.matches\r
  63   with\r
  64   | Not_found -> (id,[entry]) :: p.matches in\r
  65  {p with matches=matches}\r
  66 ;;\r
  67 \r
  68 let free_in v =\r
  69  let rec aux level = function\r
  70  | V v' -> v + level = v'\r
  71  | A(t1,t2) -> (aux level t1) || (aux level t2)\r
  72  | L t -> aux (level+1) t\r
  73  | LM(ts,_,_) -> List.fold_left (fun a b -> a || aux (level+1) b) false ts\r
  74  | B -> false\r
  75  | P -> false\r
  76  in aux 0\r
  77 ;;\r
  78 \r
  79 let rec is_inert =\r
  80  function\r
  81  | A(t,_) -> is_inert t\r
  82  | L _ | LM _ | B -> false\r
  83  | _ -> true\r
  84 ;;\r
  85 \r
  86 let is_var = function V _ -> true | _ -> false;;\r
  87 let is_lambda = function L _ -> true | _ -> false;;\r
  88 let is_pacman = function P -> true | _ -> false;;\r
  89 \r
  90 let rec subst level delift sub p =\r
  91  function\r
  92  | 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
  93  | L t -> let p, t = subst (level + 1) delift sub p t in p, L t\r
  94  | A (t1,t2) ->\r
  95   let p, t1 = subst level delift sub p t1 in\r
  96   let p, t2 = subst level delift sub p t2 in\r
  97   if t1 = B || t2 = B then p, B else\r
  98   if level = 0 then mk_app p t1 t2 else p, A (t1, t2)\r
  99  | LM (ts, liftno, id) ->\r
 100    let p, ts =\r
 101     let rec aux p = function\r
 102     | [] -> p, []\r
 103     | t::ts ->\r
 104      let p, ts = aux p ts in\r
 105      let p, t = subst (level+1) delift sub p t in\r
 106      p, t::ts in\r
 107     aux p ts in\r
 108    p, LM(ts, liftno, id)\r
 109  | B -> p, B\r
 110  | P -> p, P\r
 111 and mk_app p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
 112  | L t1 ->\r
 113   let p = if is_inert t2 && not (is_var t2) && free_in 0 t1 then {p with conv=t2::p.conv} else p in\r
 114    subst 0 true (0, t2) p t1\r
 115  | LM(ts,liftno,id) ->\r
 116   let p, t = mk_apps p t2 (List.map (lift ~-1) ts) in\r
 117   if t = B\r
 118    then p, B\r
 119    else\r
 120     let p, cont = freshvar p in\r
 121     let newvar = V cont in\r
 122     let p = add_to_match p id (t,newvar) in\r
 123       p, newvar\r
 124  | B\r
 125  | _ when t2 = B -> p, B\r
 126  | t1 -> p, A (t1, t2)\r
 127 and mk_apps p t =\r
 128  function\r
 129  | [] -> p, t\r
 130  | t'::ts -> let p, t = mk_app p t t' in mk_apps p t ts\r
 131 and lift n = function\r
 132  | V m -> V (m + n)\r
 133  | L t -> L (lift n t)\r
 134  | A (t1, t2) -> A (lift n t1, lift n t2)\r
 135  | LM (ts, liftno, id) -> LM (List.map (lift n) ts, n + liftno, id)\r
 136  | B -> B\r
 137  | P -> P\r
 138  ;;\r
 139 \r
 140 let subst = subst 0 false;;\r
 141 \r
 142 let mk_lambda t = L (lift 1 t) ;;\r
 143 \r
 144 let subst_many sub =\r
 145  let rec aux p = function\r
 146  | [] -> p, []\r
 147  | t::tms ->\r
 148   let p, t = subst sub p t in\r
 149   let p, tms = aux p tms in\r
 150   p, t :: tms\r
 151  in aux\r
 152 ;;\r
 153 \r
 154 let rec subst_in_matches sub p =\r
 155  function\r
 156  | [] -> p, []\r
 157  | (v, branches) :: ms->\r
 158   let a, b = List.split branches in\r
 159   let p, a = subst_many sub p a in\r
 160   let p, b = subst_many sub p b in\r
 161   let branches = List.combine a b in\r
 162   let p, ms = subst_in_matches sub p ms in\r
 163   p, (v, branches) :: ms\r
 164 ;;\r
 165 \r
 166 let subst_in_problem (sub: var * t) (p: problem) =\r
 167 (* print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " " ^ string_of_t p (snd sub)); *)\r
 168  let p', div = subst sub p p.div in\r
 169  let p = {p' with conv=p.conv} in\r
 170  let p, conv = subst_many sub p p.conv in\r
 171  let p, matches = subst_in_matches sub p p.matches in\r
 172  {p with div=div; conv=conv; matches=matches; sigma=sub::p.sigma}\r
 173 ;;\r
 174 \r
 175 (* FIXME *)\r
 176 let unify_terms p t1 t2 =\r
 177  match t1 with\r
 178  | V v -> subst_in_problem (v, t2) p\r
 179  | _ -> problem_fail p "The collapse of a match came after too many steps :(";;\r
 180 \r
 181 let rec unify p =\r
 182  let rec give_duplicates =\r
 183   let rec aux' t = function\r
 184   | [] -> [], None\r
 185   | (t',c')::ts -> if t = t' then ts, Some c' else (\r
 186    let ts, res = aux' t ts in (t',c')::ts, res) in\r
 187   let rec aux = function\r
 188    | [] -> [], None\r
 189    | (t,c)::rest -> (\r
 190     match aux' t rest with\r
 191     | rest, None -> aux rest\r
 192     | rest, Some c' -> (t,c)::rest, Some (c', c)\r
 193     ) in\r
 194   function\r
 195   | [] -> [], None\r
 196   | (orig,branches) :: ms ->\r
 197    match aux branches with\r
 198    | _, None -> let ms, res = give_duplicates ms in (orig,branches) :: ms, res\r
 199    | branches', Some subst -> (orig,branches') :: ms, Some subst in\r
 200  let matches, vars_to_be_unified = give_duplicates p.matches in\r
 201  let p = {p with matches=matches} in\r
 202  match vars_to_be_unified with\r
 203   | None -> p\r
 204   | Some(t', t) ->\r
 205    (* print_endline ("> unify " ^ string_of_t p (t') ^ " with " ^ string_of_t p t); *)\r
 206    unify (unify_terms p t' t)\r
 207 ;;\r
 208 \r
 209 let problem_done p =\r
 210   let all_separated = List.for_all (fun (_, lst) -> List.length lst = 1 || List.for_all (fun (t,_) -> is_var t) lst) p.matches in\r
 211   all_separated && p.div = B\r
 212 ;;\r
 213 \r
 214 exception Done;;\r
 215 \r
 216 let sanity p =\r
 217  (* Sanity checks: *)\r
 218  if is_lambda p.div || is_pacman p.div then problem_fail p "p.div converged" ;\r
 219  List.iter (function | B -> problem_fail p "p.conv diverged" | _ -> ()) p.conv;\r
 220  if not (List.for_all (fun (_, lst) -> List.for_all (fun (t,_) -> is_inert t) lst) p.matches)\r
 221   then problem_fail p "Lambda in a match: k was not big enough?";\r
 222 \r
 223  (* Remove lambdas from conv TODO remove duplicates *)\r
 224  let conv = List.filter is_inert p.conv in\r
 225  let p = {p with conv=conv} in\r
 226  (* unify! :( *)\r
 227  let p = unify p in\r
 228  print_endline (string_of_problem p);\r
 229  if problem_done p then raise Done else p\r
 230 ;;\r
 231 \r
 232 let ignore var n p =\r
 233 print_endline (\r
 234  "--- EAT on " ^ string_of_t p (V var)\r
 235  ^ " (of:" ^ string_of_int n ^ ")");\r
 236  let rec aux m t =\r
 237   if m = 0\r
 238    then lift n t\r
 239    else L (aux (m-1) t) in\r
 240  let subst = var, aux n (V var) in\r
 241  sanity (subst_in_problem subst p)\r
 242 ;;\r
 243 \r
 244 let explode' var p =\r
 245  print_endline (\r
 246  "--- EXPLODE on " ^ string_of_t p (V var)\r
 247  );\r
 248  let subst = var, B in\r
 249  sanity (subst_in_problem subst p)\r
 250  ;;\r
 251 \r
 252 let explode p =\r
 253  match p.div with\r
 254  | V var -> explode' var p\r
 255  | _ -> problem_fail p "premature explosion"\r
 256 ;;\r
 257 \r
 258 let step var p =\r
 259  print_endline (\r
 260   "--- STEP on " ^ string_of_t p (V var));\r
 261  let subst = var, LM([], 0, var) in\r
 262  sanity (subst_in_problem subst p)\r
 263 ;;\r
 264 \r
 265 let id var p =\r
 266  print_endline (\r
 267   "--- ID on " ^ string_of_t p (V var));\r
 268  let subst = var, L(V 0) in\r
 269  sanity (subst_in_problem subst p)\r
 270 ;;\r
 271 \r
 272 let apply var appk p =\r
 273  print_endline (\r
 274   "--- APPLY_CONSTS on " ^ string_of_t p (V var)\r
 275   ^ " (special_k:" ^ string_of_int appk ^ ")");\r
 276  let rec mk_freshvars n p =\r
 277   if n = 0\r
 278    then p, []\r
 279    else\r
 280     let p, vs = mk_freshvars (n-1) p in\r
 281     let p, v = freshvar p in\r
 282     p, V(v)::vs in\r
 283  let p, vars = mk_freshvars appk p in\r
 284  let p, t = mk_apps p (V 0) (List.map (lift 1) vars) in\r
 285  let t = L (A (lift 1 (V var), t))  in\r
 286  let subst = var, t in\r
 287  sanity (subst_in_problem subst p)\r
 288 ;;\r
 289 \r
 290 let perm var n p =\r
 291  print_endline (\r
 292   "--- PERM on " ^ string_of_t p (V var)\r
 293   ^ " (of:" ^ string_of_int n ^ ")");\r
 294  (* let p, v = freshvar p in *)\r
 295  let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in\r
 296  let rec aux m t =\r
 297   if m = 0\r
 298    then aux' (n-1) t\r
 299    else L (aux (m-1) t) in\r
 300  let t = aux n (lift n (V var)) in\r
 301  let subst = var, t in\r
 302  sanity (subst_in_problem subst p)\r
 303 ;;\r
 304 \r
 305 (* TODO:\r
 306 - cosi' come e' possibile unificare rami di branch solo se vanno -> a variabili,\r
 307   allo stesso modo e' possibile ignorare dei rami se vanno in variabili, e quelle variabili\r
 308   vengono sostituite ovunque: con bombe in conv e con pacman in div\r
 309 *)\r
 310 (* let forget var n p =\r
 311  let remove_from_branch p var n = ... in\r
 312  let p, (tm, c) = remove_from_branch p var n in\r
 313  print_endline (\r
 314   "--- FORGET " ^ string_of_t p tm ^ " from the match of " ^ string_of_t p (V var)\r
 315   ^ " (of:" ^ string_of_int n ^ ")");\r
 316  sanity p\r
 317 ;; *)\r
 318 \r
 319 let parse strs =\r
 320  let dummy_p = {freshno=0; div=V 0; conv=[]; matches=[]; sigma=[]} in\r
 321   let rec aux level = function\r
 322   | Parser.Lam t -> L (aux (level + 1) t)\r
 323   | Parser.App (t1, t2) ->\r
 324    if level = 0 then snd (mk_app dummy_p (aux level t1) (aux level t2))\r
 325     else A(aux level t1, aux level t2)\r
 326   | Parser.Var v -> V v\r
 327   in let (tms, free) = Parser.parse_many strs\r
 328   in (List.map (aux 0) tms, free)\r
 329 ;;\r
 330 \r
 331 let magic6 div conv cmds =\r
 332  print_hline ();\r
 333  let all_tms, var_names = parse (div :: conv) in\r
 334  let div, conv = List.hd all_tms, List.tl all_tms in\r
 335  let freshno = 1 + List.length var_names in\r
 336  let p = {freshno; div; conv; matches=[]; sigma=[]} in\r
 337  let p = try\r
 338   let subst = Util.index_of "BOMB" var_names, L B in\r
 339   let p = subst_in_problem subst p in p\r
 340   with Not_found -> p in\r
 341  let p = sanity p in\r
 342  try\r
 343   problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
 344  with\r
 345  | Done -> ()\r
 346 ;;\r
 347 \r
 348 let interactive div conv cmds =\r
 349  print_hline ();\r
 350  let all_tms, var_names = parse (div :: conv) in\r
 351  let div, conv = List.hd all_tms, List.tl all_tms in\r
 352  let freshno = 1 + List.length var_names in\r
 353  let p = {freshno; div; conv; matches=[]; sigma=[]} in\r
 354  let p = try\r
 355   let subst = Util.index_of "BOMB" var_names, L B in\r
 356   let p = subst_in_problem subst p in p\r
 357   with Not_found -> p in\r
 358  let p = sanity p in\r
 359  let p = List.fold_left (|>) p cmds in\r
 360  let rec f p cmds =\r
 361   let nth spl n = int_of_string (List.nth spl n) in\r
 362   let read_cmd () =\r
 363    let s = read_line () in\r
 364    let spl = Str.split (Str.regexp " +") s in\r
 365    s, let uno = List.hd spl in\r
 366     try if uno = "explode" then explode\r
 367     else if uno = "ignore" then ignore (nth spl 1) (nth spl 2)\r
 368     else if uno = "step" then step (nth spl 1)\r
 369     else if uno = "perm" then perm (nth spl 1) (nth spl 2)\r
 370     else if uno = "apply" then apply (nth spl 1) (nth spl 2)\r
 371     else if uno = "id" then id (nth spl 1)\r
 372     else failwith "unknown"\r
 373     with Failure _ -> print_endline "Wrong input."; (fun x -> x) in\r
 374   let str, cmd = read_cmd () in\r
 375   let cmds = str::cmds in\r
 376   try\r
 377    let p = cmd p in f p cmds\r
 378   with\r
 379   | Done -> List.iter print_endline (List.rev cmds)\r
 380  in f p []\r
 381 ;;\r
 382 \r
 383 let _ = magic6\r
 384  "x x"\r
 385  [ "_. BOMB" ]\r
 386  [ ignore 1 1; explode ]\r
 387 ;;\r
 388 \r
 389  let _ = magic6\r
 390     "x y BOMB b"\r
 391   [ "x BOMB y c" ]\r
 392   [ perm 1 3; step 1 ; ignore 8 2; explode; ];;\r
 393 \r
 394 let _ = magic6\r
 395    "x BOMB a1 c"\r
 396  [ "x y BOMB d"; "x BOMB a2 c" ]\r
 397  [ perm 1 3 ; step 1 ; step 12; ignore 13 1; explode; ]\r
 398 ;;\r
 399 \r
 400 let _ = magic6\r
 401  "x (x x)"\r
 402  [ "x x" ; "x x x" ] [\r
 403  apply 1 1;\r
 404  step 1;\r
 405  explode;\r
 406  step 9;\r
 407 ];;\r
 408 \r
 409 let _ = magic6\r
 410  "x (_.BOMB)"\r
 411  [ "x (_._. BOMB)" ]\r
 412  [ apply 1 2; ]\r
 413 ;;\r
 414 \r
 415 let _ = magic6\r
 416  "x (_.y)"\r
 417  [ "y (_. x)" ]\r
 418  [ apply 1 1; ignore 1 1;  explode; ]\r
 419 ;;\r
 420 \r
 421 let _ = magic6\r
 422  "y (x a1 BOMB c) (x BOMB b1 d)"\r
 423  [ "y (x a2 BOMB c) (x BOMB b1 d)";\r
 424  "y (x a1 BOMB c) (x BOMB b2 d)";]\r
 425  [ perm 2 3; step 2; step 17; perm 16 2; step 16; ignore 19 1; ignore 20 1; ignore 22 1; ignore 23 1; step 1; step 26; explode; ]\r
 426 ;;\r
 427 \r
 428 let _ = magic6\r
 429  "z (y x)"\r
 430  [ "z (y (x.x))"; "y (_. BOMB)" ]\r
 431  [ apply 2 1; step 3; explode' 8; ]\r
 432 ;;\r
 433 \r
 434 let _ = magic6\r
 435  "y x"\r
 436  [ "y (x.x)"; "x (_. BOMB)" ]\r
 437  [ apply 1 1; ignore 2 1; step 1; explode; ]\r
 438 ;;\r
 439 \r
 440 let _ = magic6\r
 441  "z (y x)"\r
 442  [ "z (y (x.x))"; "y (_. BOMB)" ]\r
 443  [ step 1; explode; apply 2 1; id 2; ignore 3 1; ]\r
 444 ;;\r
 445 \r
 446 let _ = magic6\r
 447  "y (x a)"\r
 448  [ "y (x b)"; "x BOMB" ] [\r
 449  id 2;\r
 450  step 1;\r
 451  explode;\r
 452 ];;\r
 453 \r
 454 magic6\r
 455  "y (x a)" [ "y (x b)"; "x BOMB"; "y a" ]\r
 456  [\r
 457  apply 1 1;\r
 458  perm 2 2;\r
 459  perm 2 2;\r
 460  step 3;\r
 461  apply 2 1;\r
 462  ignore 4 1;\r
 463  step 2;\r
 464  ignore 12 1;\r
 465  ignore 13 1;\r
 466  step 1;\r
 467  explode;\r
 468 ];;\r
 469 \r
 470 interactive\r
 471   "y (x a)"\r
 472 [ "y (x b)"; "x BOMB"; "y a" ] [];;\r
 473 \r
 474 print_endline "ALL DONE. "\r