1 let print_hline = Console.print_hline;;
\r
10 t list (* body of the match *)
\r
11 * int (* explicit liftno *)
\r
12 * int (* variable which originated this match (id) *)
\r
23 ; matches : (var (* variable originating this match *) * (bool (* term comes from div*) * (t (* term to discriminate *) * t (* continuation *))) list) list
\r
24 ; sigma : (var * t) list (* substitutions *)
\r
28 let bound_vars = ["x"; "y"; "z"; "z1"; "z2"] in
\r
29 let rec aux level = function
\r
30 | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)
\r
31 | A (t1,t2) -> "("^aux level t1^" "^aux level t2^")"
\r
32 | L t -> "(\\" ^ aux (level+1) (V 0) ^ ". " ^ aux (level+1) t ^ ")"
\r
33 | LM (ts,liftno,id) -> "[match orig="^aux 0 (V id)^"]"
\r
40 let bound_vars = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in
\r
41 let rec string_of_term_w_pars level = function
\r
42 | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)
\r
43 | A _ as t -> "(" ^ string_of_term_no_pars_app level t ^ ")"
\r
44 | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"
\r
45 | LM (ts,liftno,id) -> "[match orig="^ string_of_term_w_pars 0 (V id)^"]"
\r
48 and string_of_term_no_pars_app level = function
\r
49 | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)
\r
50 | _ as t -> string_of_term_w_pars level t
\r
51 and string_of_term_no_pars_lam level = function
\r
52 | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)
\r
53 | _ as t -> string_of_term_no_pars level t
\r
54 and string_of_term_no_pars level = function
\r
55 | L _ as t -> string_of_term_no_pars_lam level t
\r
56 | _ as t -> string_of_term_no_pars_app level t
\r
57 in string_of_term_no_pars 0
\r
60 let string_of_problem p =
\r
62 "[DV] " ^ String.concat "\n " (List.map (string_of_t p) p.div);
\r
63 "[CV] " ^ String.concat "\n " (List.map (string_of_t p) p.conv);
\r
65 ] @ 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
66 (* ^" -> " ^ string_of_t p c *)
\r
67 ) lst) p.matches @ [""] in
\r
68 String.concat "\n" lines
\r
71 let problem_fail p reason =
\r
72 print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";
\r
73 print_endline (string_of_problem p);
\r
77 let freshvar ({freshno} as p) =
\r
78 {p with freshno=freshno+1}, freshno+1
\r
81 let add_to_match p id entry =
\r
83 let _ = List.assoc id p.matches in
\r
84 List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry::lst) ) p.matches
\r
86 | Not_found -> (id,[entry]) :: p.matches in
\r
90 let var_occurs_in v =
\r
91 let rec aux level = function
\r
92 | V v' -> v + level = v'
\r
93 | A(t1,t2) -> (aux level t1) || (aux level t2)
\r
94 | L t -> aux (level+1) t
\r
95 | LM(ts,_,_) -> List.fold_left (fun a b -> a || aux (level+1) b) false ts
\r
103 | A(t,_) -> is_inert t
\r
105 | L _ | LM _ | B | P -> false
\r
108 let is_var = function V _ -> true | _ -> false;;
\r
109 let is_lambda = function L _ -> true | _ -> false;;
\r
110 let is_pacman = function P -> true | _ -> false;;
\r
112 let rec subst isdiv level delift sub p =
\r
114 | 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
115 | L t -> let p, t = subst isdiv (level + 1) delift sub p t in p, L t
\r
117 let p, t1 = subst isdiv level delift sub p t1 in
\r
118 let p, t2 = subst isdiv level delift sub p t2 in
\r
119 if t1 = B || t2 = B then p, B else
\r
120 if level = 0 then mk_app isdiv p t1 t2 else p, A (t1, t2)
\r
121 | LM (ts, liftno, id) ->
\r
123 let rec aux p = function
\r
126 let p, ts = aux p ts in
\r
127 let p, t = subst isdiv (level+1) delift sub p t in
\r
130 p, LM(ts, liftno, id)
\r
133 and mk_app isdiv p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with
\r
135 (* FIXME BUG HERE! *)
\r
136 if is_inert t2 && (match t2 with V v -> v > p.orig_freshno | _ -> true ) && not (var_occurs_in 0 t1)
\r
137 then (if isdiv then {p with div=p.div @ [t2]} else {p with conv=p.conv @ [t2]}), lift (-1) t1
\r
138 else subst isdiv 0 true (0, t2) p t1
\r
139 | LM(ts,liftno,id) ->
\r
140 let p, t = mk_apps isdiv p t2 (List.map (lift ~-1) ts) in
\r
144 let p, cont = freshvar p in
\r
145 let newvar = V cont in
\r
146 let p = add_to_match p id (isdiv,(t,newvar)) in
\r
149 | _ when t2 = B -> p, B
\r
150 | t1 -> p, A (t1, t2)
\r
151 and mk_apps isdiv p t =
\r
154 | t'::ts -> let p, t = mk_app isdiv p t t' in mk_apps isdiv p t ts
\r
158 | V m -> V (if m >= n' then m + n else m)
\r
159 | L t -> L (aux (n'+1) t)
\r
160 | A (t1, t2) -> A (aux n' t1, aux n' t2)
\r
161 | LM (ts, liftno, id) -> LM (List.map (aux (n'+1)) ts, n + liftno, id)
\r
167 let subst isdiv = subst isdiv 0 false;;
\r
169 let mk_lambda t = L (lift 1 t) ;;
\r
171 let subst_many b sub =
\r
172 let rec aux p = function
\r
175 let p, t = subst b sub p t in
\r
176 let p, tms = aux p tms in
\r
181 let rec subst_in_matches sub p =
\r
184 | (v, branches) :: ms->
\r
185 let a, b = List.split branches in
\r
186 let b, c = List.split b in
\r
187 let p, b = subst_many false sub p b in
\r
188 let p, c = subst_many false sub p c in
\r
189 let b = List.combine b c in
\r
190 let branches = List.combine a b in
\r
191 let p, ms = subst_in_matches sub p ms in
\r
192 p, (v, branches) :: ms
\r
195 let subst_in_problem (sub: var * t) (p: problem) =
\r
196 (* print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " " ^ string_of_t p (snd sub)); *)
\r
197 let div, conv = p.div, p.conv in
\r
198 let p = {p with div=[]; conv=[]} in
\r
199 let p, div' = subst_many true sub p div in
\r
200 let p, conv' = subst_many false sub p conv in
\r
201 let p, matches = subst_in_matches sub p p.matches in
\r
202 let p = {p with div=div'@p.div; conv=conv'@p.conv; matches} in
\r
203 (* print_endline ("after sub: \n" ^ string_of_problem p); *)
\r
204 {p with sigma=sub::p.sigma}
\r
208 let unify_terms p t1 t2 =
\r
210 | V v -> subst_in_problem (v, t2) p
\r
211 | _ -> problem_fail p "The collapse of a match came after too many steps :(";;
\r
214 let rec give_duplicates =
\r
215 let rec aux' t = function
\r
217 | (b',(t',c'))::ts -> if t = t' (* FIXME! eta-eq here *)then ts, Some (b',c') else (
\r
218 let ts, res = aux' t ts in (b',(t',c'))::ts, res) in
\r
219 let rec aux = function
\r
221 | (b,(t,c))::rest -> (
\r
222 match aux' t rest with
\r
223 | rest, None -> aux rest
\r
224 | rest, Some (b',c') -> ((if not b' then false else b),(t,c))::rest, Some (c', c)
\r
228 | (orig,branches) :: ms ->
\r
229 match aux branches with
\r
230 | _, None -> let ms, res = give_duplicates ms in (orig,branches) :: ms, res
\r
231 | branches', Some subst -> (orig,branches') :: ms, Some subst in
\r
232 let matches, vars_to_be_unified = give_duplicates p.matches in
\r
233 let p = {p with matches=matches} in
\r
234 match vars_to_be_unified with
\r
237 (* print_endline ("> unify " ^ string_of_t p (t') ^ " with " ^ string_of_t p t); *)
\r
238 unify (unify_terms p t' t)
\r
241 let problem_done p =
\r
242 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
243 all_separated && List.exists ((=) B) p.div
\r
246 let free_vars p t =
\r
247 let rec aux level = function
\r
248 | V v -> if v >= level then [v] else []
\r
249 | A(t1,t2) -> (aux level t1) @ (aux level t2)
\r
250 | L t -> aux (level+1) t
\r
251 | LM(ts,_,id) -> (List.concat (List.map (aux level) ts)) @ (
\r
252 let lst = List.assoc id p.matches in
\r
253 List.concat (List.map (fun (_,(t1,t2)) -> (aux 0 t1) @ (aux 0 t2)) lst)
\r
257 in Util.sort_uniq (aux 0 t)
\r
260 let visible_vars p t =
\r
261 let rec aux = function
\r
263 | A(t1,t2) -> (aux t1) @ (aux t2)
\r
265 | LM(ts,_,id) -> (List.concat (List.map aux ts)) @ (
\r
266 let lst = List.assoc id p.matches in
\r
267 List.concat (List.map (fun (_,(t1,t2)) -> (aux t1) @ (aux t2)) lst)
\r
271 in Util.sort_uniq (aux t)
\r
274 let forget_variable var p =
\r
275 let p', div = subst_many true (var, P) p p.div in
\r
276 let p = {p' with conv=p.conv} in
\r
277 let p, conv = subst_many false (var, B) p p.conv in
\r
278 let p, matches = subst_in_matches (var, B) p p.matches in
\r
279 {p with div; conv; matches; sigma=p.sigma}
\r
281 let rec remove_divergent_discriminators p =
\r
282 let f = fun (b,(t,_)) -> b && (t = B || is_lambda t) in
\r
284 let v,l = List.find (fun (_,lst) -> List.exists f lst) p.matches in
\r
285 let (_,(_,c)) as entry = List.find f l in
\r
286 let l = List.filter ((<>) entry) l in
\r
287 let matches = List.map (fun (v', l') -> v', if v' = v then l else l') p.matches in
\r
288 let vars = free_vars p c in
\r
289 let p = {p with matches} in
\r
290 List.fold_right forget_variable vars p
\r
291 with Not_found -> p
\r
297 (* try to fix divergent discriminators *)
\r
298 let p = remove_divergent_discriminators p in
\r
299 (* Remove lambdas from conv TODO remove duplicates *)
\r
300 let div = List.filter (function | P | L _ -> false | _ -> true) p.div in
\r
301 let conv = List.filter (function | B | V _ | A _ -> true | _ -> false) p.conv in
\r
302 let p = {p with div;conv} in
\r
303 (* Sanity checks: *)
\r
304 if p.div = [] then problem_fail p "p.div converged";
\r
305 if List.mem B p.conv then problem_fail p "p.conv diverged";
\r
306 if not (List.for_all (fun (_, lst) -> List.for_all (fun (b,(t,_)) -> is_inert t) lst) p.matches)
\r
307 then problem_fail p "Unsolvable discrimination";
\r
311 print_endline (string_of_problem p); (* non cancellare *)
\r
312 if problem_done p then raise Done else p
\r
315 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
\r
317 let ignore var n p =
\r
318 print_cmd "EAT" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
\r
322 else L (aux (m-1) t) in
\r
323 let p, fresh = freshvar p in
\r
324 let subst = var, aux n (V fresh) in
\r
325 sanity (subst_in_problem subst p)
\r
329 let fv1 = List.concat (List.map (visible_vars p) p.div) in
\r
330 let fv2 = List.concat (List.map (visible_vars p) p.conv) in
\r
331 let fv = List.filter (fun x -> not (List.mem x fv2)) fv1 in
\r
332 let fv = List.filter ((<) p.orig_freshno) fv in
\r
335 print_cmd "EXPLODE" ("on " ^ string_of_t p (V var));
\r
336 let subst = var, B in
\r
337 sanity (subst_in_problem subst p)
\r
338 | _ -> problem_fail p "premature explosion"
\r
342 print_cmd "STEP" ("on " ^ string_of_t p (V var));
\r
343 let subst = var, LM([], 0, var) in
\r
344 sanity (subst_in_problem subst p)
\r
348 print_cmd "ID" ("on " ^ string_of_t p (V var));
\r
349 let subst = var, L(V 0) in
\r
350 sanity (subst_in_problem subst p)
\r
353 let apply var appk p =
\r
355 (string_of_t p (V var) ^ " applies no." ^ string_of_int appk ^ " fresh variables");
\r
356 let rec mk_freshvars n p =
\r
360 let p, vs = mk_freshvars (n-1) p in
\r
361 let p, v = freshvar p in
\r
363 let p, vars = mk_freshvars appk p in
\r
364 let p, t = mk_apps false p (V 0) (List.map (lift 1) vars) in
\r
365 let t = L (A (lift 1 (V var), t)) in
\r
366 let subst = var, t in
\r
367 sanity (subst_in_problem subst p)
\r
371 print_cmd "PERM" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
\r
372 let p, v = freshvar p in
\r
373 let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in
\r
377 else L (aux (m-1) t) in
\r
378 let t = aux n (lift n (V v)) in
\r
379 let subst = var, t in
\r
380 sanity (subst_in_problem subst p)
\r
384 - cosi' come e' possibile unificare rami di branch solo se vanno -> a variabili,
\r
385 allo stesso modo e' possibile ignorare dei rami se vanno in variabili, e quelle variabili
\r
386 vengono sostituite ovunque: con bombe in conv e con pacman in div
\r
388 let forget var no p =
\r
390 let l = List.assoc var p.matches in
\r
391 let (b,(tm,c)) = List.nth l no in
\r
392 let l = List.mapi (fun n x -> if n = no then (b,(B,c)) else x) l in
\r
393 let matches = List.map (fun (v,lst) -> v, if v = var then l else lst) p.matches in
\r
394 let p = {p with matches} in
\r
395 print_cmd "FORGET" (string_of_t p tm ^ " from the match of " ^ string_of_t p (V var));
\r
400 "--- FORGET " ^ string_of_t p tm ^ " from the match of " ^ string_of_t p (V var));
\r
401 let p = forget_variable var p in
\r
403 | _ -> print_endline "too late to forget that term"; p
\r
405 with Failure "nth" ->
\r
406 print_endline "wtf?"; p
\r
410 let dummy_p = {orig_freshno=0; freshno=0; div=[]; conv=[]; matches=[]; sigma=[]} in
\r
411 let rec aux level = function
\r
412 | Parser.Lam t -> L (aux (level + 1) t)
\r
413 | Parser.App (t1, t2) ->
\r
414 if level = 0 then snd (mk_app false dummy_p (aux level t1) (aux level t2))
\r
415 else A(aux level t1, aux level t2)
\r
416 | Parser.Var v -> V v
\r
417 in let (tms, free) = Parser.parse_many strs
\r
418 in (List.map (aux 0) tms, free)
\r
421 let rec list_split n =
\r
424 | x::xs as l -> if n = 0 then [], l else let a, b = list_split (n-1) xs in x::a, b
\r
427 let magic6 div conv cmds =
\r
429 let all_tms, var_names = parse (div @ conv) in
\r
430 let div, conv = list_split (List.length div) all_tms in
\r
431 let varno = List.length var_names in
\r
432 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in
\r
434 let subst = Util.index_of "BOMB" var_names, L B in
\r
435 let p = subst_in_problem subst p in p
\r
436 with Not_found -> p in
\r
437 let p = sanity p in
\r
439 problem_fail (List.fold_left (|>) p cmds) "Problem not completed"
\r
444 let interactive div conv cmds =
\r
446 let all_tms, var_names = parse (div @ conv) in
\r
447 let div, conv = list_split (List.length div) all_tms in
\r
448 let varno = List.length var_names in
\r
449 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in
\r
450 (* activate bombs *)
\r
452 let subst = Util.index_of "BOMB" var_names, L B in
\r
453 subst_in_problem subst p
\r
454 with Not_found -> p in
\r
455 (* activate pacmans *)
\r
457 let subst = Util.index_of "PACMAN" var_names, P in
\r
458 let p = subst_in_problem subst p in
\r
459 (print_endline ("after subst in problem " ^ string_of_problem p); p)
\r
460 with Not_found -> p in
\r
461 (* initial sanity check *)
\r
462 let p = sanity p in
\r
463 let p = List.fold_left (|>) p cmds in
\r
465 let nth spl n = int_of_string (List.nth spl n) in
\r
467 let s = read_line () in
\r
468 let spl = Str.split (Str.regexp " +") s in
\r
469 s, let uno = List.hd spl in
\r
470 try if uno = "explode" then explode
\r
471 else if uno = "ignore" then ignore (nth spl 1) (nth spl 2)
\r
472 else if uno = "step" then step (nth spl 1)
\r
473 else if uno = "perm" then perm (nth spl 1) (nth spl 2)
\r
474 else if uno = "apply" then apply (nth spl 1) (nth spl 2)
\r
475 else if uno = "forget" then forget (nth spl 1) (nth spl 2)
\r
476 else if uno = "id" then id (nth spl 1)
\r
477 else failwith "Wrong input."
\r
478 with Failure s -> print_endline s; (fun x -> x) in
\r
479 let str, cmd = read_cmd () in
\r
480 let cmds = (" " ^ str ^ ";")::cmds in
\r
482 let p = cmd p in f p cmds
\r
484 | Done -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)
\r
491 [ ignore 1 1; explode ]
\r
497 [ perm 1 3; step 8 ; explode; ];;
\r
501 [ "x y BOMB d"; "x BOMB a2 c" ]
\r
502 [ perm 1 3 ; step 10 ; step 13; explode; ]
\r
507 [ "x x" ; "x x x" ] [
\r
516 [ "x (_._. BOMB)" ]
\r
523 [ apply 1 1; ignore 1 1; explode; ]
\r
527 ["y (x a1 BOMB c) (x BOMB b1 d)"]
\r
528 [ "y (x a2 BOMB c) (x BOMB b1 d)";
\r
529 "y (x a1 BOMB c) (x BOMB b2 d)";] [
\r
547 [ "z (y (x.x))"; "y (_. BOMB)" ]
\r
548 [ apply 2 1; step 3; explode; ]
\r
553 [ "y (x.x)"; "x (_. BOMB)" ]
\r
554 [ apply 1 1; ignore 2 1; step 1; explode; ]
\r
559 [ "z (y (x.x))"; "y (_. BOMB)" ]
\r
560 [ step 1; explode; apply 2 1; id 2; ignore 3 1; ]
\r
565 [ "y (x b)"; "x BOMB" ] [
\r
572 ["y (x a)"] [ "y (x b)"; "x BOMB"; "y a" ]
\r
581 [ "y (b c)"; "y (x a)"; "y (x b)"; "x BOMB" ] *)
\r
584 ["x a (x (a.y BOMB))"]
\r
585 [ "x b"; "x (y c)"; "x (y d)" ]
\r
593 (* ma si puo' fare anche senza forget *) *)
\r
597 (* dipendente dalla codifica? no, ma si risolve solo con id *)
\r
599 ["y a"] ["y b"; "x (y (_.BOMB))"]
\r
605 (* [id 1; explode];; *)
\r
608 ["PACMAN (x x x)"] ["PACMAN (x x)"]
\r
615 print_endline "ALL DONE. "
\r