\r
\r
type problem = {\r
- freshno : int\r
- ; div : t\r
+ orig_freshno: int\r
+ ; freshno : int\r
+ ; div : t list\r
; conv : t list\r
- ; matches : (var (* variable originating this match *) * (t (* term to discriminate *) * t (* continuation *)) list) list\r
+ ; matches : (var (* variable originating this match *) * (bool (* term comes from div*) * (t (* term to discriminate *) * t (* continuation *))) list) list\r
; sigma : (var * t) list (* substitutions *)\r
}\r
\r
in aux 0\r
;;\r
\r
+let string_of_t p =\r
+ let bound_vars = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in\r
+ let rec string_of_term_w_pars level = function\r
+ | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)\r
+ | A _ as t -> "(" ^ string_of_term_no_pars_app level t ^ ")"\r
+ | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"\r
+ | LM (ts,liftno,id) -> "[match orig="^ string_of_term_w_pars 0 (V id)^"]"\r
+ | B -> "BOT"\r
+ | P -> "PAC"\r
+ and string_of_term_no_pars_app level = function\r
+ | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)\r
+ | _ as t -> string_of_term_w_pars level t\r
+ and string_of_term_no_pars_lam level = function\r
+ | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)\r
+ | _ as t -> string_of_term_no_pars level t\r
+ and string_of_term_no_pars level = function\r
+ | L _ as t -> string_of_term_no_pars_lam level t\r
+ | _ as t -> string_of_term_no_pars_app level t\r
+ in string_of_term_no_pars 0\r
+;;\r
+\r
let string_of_problem p =\r
let lines = [\r
- "[DV] " ^ string_of_t p p.div;\r
+ "[DV] " ^ String.concat "\n " (List.map (string_of_t p) p.div);\r
"[CV] " ^ String.concat "\n " (List.map (string_of_t p) p.conv);\r
- "" ;\r
- ] @ Util.concat_map (fun (_, lst) -> "[<>]" :: List.map (fun (t,c) -> " " ^ string_of_t p t\r
+ (* "" ; *)\r
+ ] @ 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
(* ^" -> " ^ string_of_t p c *)\r
) lst) p.matches @ [""] in\r
String.concat "\n" lines\r
;;\r
\r
let problem_fail p reason =\r
- print_endline " FAIL FAIL FAIL FAIL FAIL FAIL FAIL FAIL FAIL";\r
+ print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
print_endline (string_of_problem p);\r
failwith reason\r
;;\r
List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry::lst) ) p.matches\r
with\r
| Not_found -> (id,[entry]) :: p.matches in\r
- {p with matches=matches}\r
+ {p with matches}\r
;;\r
\r
-let free_in v =\r
+let var_occurs_in v =\r
let rec aux level = function\r
| V v' -> v + level = v'\r
| A(t1,t2) -> (aux level t1) || (aux level t2)\r
let rec is_inert =\r
function\r
| A(t,_) -> is_inert t\r
- | L _ | LM _ | B -> false\r
- | _ -> true\r
+ | V _ -> true\r
+ | L _ | LM _ | B | P -> false\r
;;\r
\r
let is_var = function V _ -> true | _ -> false;;\r
let is_lambda = function L _ -> true | _ -> false;;\r
let is_pacman = function P -> true | _ -> false;;\r
\r
-let rec subst level delift sub p =\r
+let rec subst isdiv level delift sub p =\r
function\r
| 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
- | L t -> let p, t = subst (level + 1) delift sub p t in p, L t\r
+ | L t -> let p, t = subst isdiv (level + 1) delift sub p t in p, L t\r
| A (t1,t2) ->\r
- let p, t1 = subst level delift sub p t1 in\r
- let p, t2 = subst level delift sub p t2 in\r
+ let p, t1 = subst isdiv level delift sub p t1 in\r
+ let p, t2 = subst isdiv level delift sub p t2 in\r
if t1 = B || t2 = B then p, B else\r
- if level = 0 then mk_app p t1 t2 else p, A (t1, t2)\r
+ if level = 0 then mk_app isdiv p t1 t2 else p, A (t1, t2)\r
| LM (ts, liftno, id) ->\r
let p, ts =\r
let rec aux p = function\r
| [] -> p, []\r
| t::ts ->\r
let p, ts = aux p ts in\r
- let p, t = subst (level+1) delift sub p t in\r
+ let p, t = subst isdiv (level+1) delift sub p t in\r
p, t::ts in\r
aux p ts in\r
p, LM(ts, liftno, id)\r
| B -> p, B\r
| P -> p, P\r
-and mk_app p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
+and mk_app isdiv p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
| L t1 ->\r
- 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
- subst 0 true (0, t2) p t1\r
+ (* FIXME BUG HERE! *)\r
+ if is_inert t2 && (match t2 with V v -> v > p.orig_freshno | _ -> true ) && not (var_occurs_in 0 t1)\r
+ then (if isdiv then {p with div=p.div @ [t2]} else {p with conv=p.conv @ [t2]}), lift (-1) t1\r
+ else subst isdiv 0 true (0, t2) p t1\r
| LM(ts,liftno,id) ->\r
- let p, t = mk_apps p t2 (List.map (lift ~-1) ts) in\r
+ let p, t = mk_apps isdiv p t2 (List.map (lift ~-1) ts) in\r
if t = B\r
then p, B\r
else\r
let p, cont = freshvar p in\r
let newvar = V cont in\r
- let p = add_to_match p id (t,newvar) in\r
+ let p = add_to_match p id (isdiv,(t,newvar)) in\r
p, newvar\r
| B\r
| _ when t2 = B -> p, B\r
| t1 -> p, A (t1, t2)\r
-and mk_apps p t =\r
+and mk_apps isdiv p t =\r
function\r
| [] -> p, t\r
- | t'::ts -> let p, t = mk_app p t t' in mk_apps p t ts\r
-and lift n = function\r
- | V m -> V (m + n)\r
- | L t -> L (lift n t)\r
- | A (t1, t2) -> A (lift n t1, lift n t2)\r
- | LM (ts, liftno, id) -> LM (List.map (lift n) ts, n + liftno, id)\r
- | B -> B\r
- | P -> P\r
+ | t'::ts -> let p, t = mk_app isdiv p t t' in mk_apps isdiv p t ts\r
+ and lift n =\r
+ let rec aux n' =\r
+ function\r
+ | V m -> V (if m >= n' then m + n else m)\r
+ | L t -> L (aux (n'+1) t)\r
+ | A (t1, t2) -> A (aux n' t1, aux n' t2)\r
+ | LM (ts, liftno, id) -> LM (List.map (aux (n'+1)) ts, n + liftno, id)\r
+ | B -> B\r
+ | P -> P\r
+ in aux 0\r
;;\r
\r
-let subst = subst 0 false;;\r
+let subst isdiv = subst isdiv 0 false;;\r
\r
let mk_lambda t = L (lift 1 t) ;;\r
\r
-let subst_many sub =\r
+let subst_many b sub =\r
let rec aux p = function\r
| [] -> p, []\r
| t::tms ->\r
- let p, t = subst sub p t in\r
+ let p, t = subst b sub p t in\r
let p, tms = aux p tms in\r
p, t :: tms\r
in aux\r
| [] -> p, []\r
| (v, branches) :: ms->\r
let a, b = List.split branches in\r
- let p, a = subst_many sub p a in\r
- let p, b = subst_many sub p b in\r
+ let b, c = List.split b in\r
+ let p, b = subst_many false sub p b in\r
+ let p, c = subst_many false sub p c in\r
+ let b = List.combine b c in\r
let branches = List.combine a b in\r
let p, ms = subst_in_matches sub p ms in\r
p, (v, branches) :: ms\r
\r
let subst_in_problem (sub: var * t) (p: problem) =\r
(* print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " " ^ string_of_t p (snd sub)); *)\r
- let p', div = subst sub p p.div in\r
- let p = {p' with conv=p.conv} in\r
- let p, conv = subst_many sub p p.conv in\r
+ let div, conv = p.div, p.conv in\r
+ let p = {p with div=[]; conv=[]} in\r
+ let p, div' = subst_many true sub p div in\r
+ let p, conv' = subst_many false sub p conv in\r
let p, matches = subst_in_matches sub p p.matches in\r
- {p with div=div; conv=conv; matches=matches; sigma=sub::p.sigma}\r
+ let p = {p with div=div'@p.div; conv=conv'@p.conv; matches} in\r
+ (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
+ {p with sigma=sub::p.sigma}\r
;;\r
\r
(* FIXME *)\r
let rec give_duplicates =\r
let rec aux' t = function\r
| [] -> [], None\r
- | (t',c')::ts -> if t = t' then ts, Some c' else (\r
- let ts, res = aux' t ts in (t',c')::ts, res) in\r
+ | (b',(t',c'))::ts -> if t = t' (* FIXME! eta-eq here *)then ts, Some (b',c') else (\r
+ let ts, res = aux' t ts in (b',(t',c'))::ts, res) in\r
let rec aux = function\r
| [] -> [], None\r
- | (t,c)::rest -> (\r
+ | (b,(t,c))::rest -> (\r
match aux' t rest with\r
| rest, None -> aux rest\r
- | rest, Some c' -> (t,c)::rest, Some (c', c)\r
+ | rest, Some (b',c') -> ((if not b' then false else b),(t,c))::rest, Some (c', c)\r
) in\r
function\r
| [] -> [], None\r
;;\r
\r
let problem_done p =\r
- 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
- all_separated && p.div = B\r
+ 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
+ all_separated && List.exists ((=) B) p.div\r
+;;\r
+\r
+let free_vars p t =\r
+ let rec aux level = function\r
+ | V v -> if v >= level then [v] else []\r
+ | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
+ | L t -> aux (level+1) t\r
+ | LM(ts,_,id) -> (List.concat (List.map (aux level) ts)) @ (\r
+ let lst = List.assoc id p.matches in\r
+ List.concat (List.map (fun (_,(t1,t2)) -> (aux 0 t1) @ (aux 0 t2)) lst)\r
+ )\r
+ | B -> []\r
+ | P -> []\r
+ in Util.sort_uniq (aux 0 t)\r
+;;\r
+\r
+let visible_vars p t =\r
+ let rec aux = function\r
+ | V v -> [v]\r
+ | A(t1,t2) -> (aux t1) @ (aux t2)\r
+ | L t -> []\r
+ | LM(ts,_,id) -> (List.concat (List.map aux ts)) @ (\r
+ let lst = List.assoc id p.matches in\r
+ List.concat (List.map (fun (_,(t1,t2)) -> (aux t1) @ (aux t2)) lst)\r
+ )\r
+ | B -> []\r
+ | P -> []\r
+ in Util.sort_uniq (aux t)\r
+;;\r
+\r
+let forget_variable var p =\r
+ let p', div = subst_many true (var, P) p p.div in\r
+ let p = {p' with conv=p.conv} in\r
+ let p, conv = subst_many false (var, B) p p.conv in\r
+ let p, matches = subst_in_matches (var, B) p p.matches in\r
+ {p with div; conv; matches; sigma=p.sigma}\r
+;;\r
+let rec remove_divergent_discriminators p =\r
+ let f = fun (b,(t,_)) -> b && (t = B || is_lambda t) in\r
+ try\r
+ let v,l = List.find (fun (_,lst) -> List.exists f lst) p.matches in\r
+ let (_,(_,c)) as entry = List.find f l in\r
+ let l = List.filter ((<>) entry) l in\r
+ let matches = List.map (fun (v', l') -> v', if v' = v then l else l') p.matches in\r
+ let vars = free_vars p c in\r
+ let p = {p with matches} in\r
+ List.fold_right forget_variable vars p\r
+ with Not_found -> p\r
;;\r
\r
exception Done;;\r
\r
let sanity p =\r
+ (* try to fix divergent discriminators *)\r
+ let p = remove_divergent_discriminators p in\r
+ (* Remove lambdas from conv TODO remove duplicates *)\r
+ let div = List.filter (function | P | L _ -> false | _ -> true) p.div in\r
+ let conv = List.filter (function | B | V _ | A _ -> true | _ -> false) p.conv in\r
+ let p = {p with div;conv} in\r
(* Sanity checks: *)\r
- if is_lambda p.div || is_pacman p.div then problem_fail p "p.div converged" ;\r
- List.iter (function | B -> problem_fail p "p.conv diverged" | _ -> ()) p.conv;\r
- if not (List.for_all (fun (_, lst) -> List.for_all (fun (t,_) -> is_inert t) lst) p.matches)\r
- then problem_fail p "Lambda in a match: k was not big enough?";\r
+ if p.div = [] then problem_fail p "p.div converged";\r
+ if List.mem B p.conv then problem_fail p "p.conv diverged";\r
+ if not (List.for_all (fun (_, lst) -> List.for_all (fun (b,(t,_)) -> is_inert t) lst) p.matches)\r
+ then problem_fail p "Unsolvable discrimination";\r
\r
- (* Remove lambdas from conv TODO remove duplicates *)\r
- let conv = List.filter is_inert p.conv in\r
- let p = {p with conv=conv} in\r
(* unify! :( *)\r
let p = unify p in\r
- print_endline (string_of_problem p);\r
+ print_endline (string_of_problem p); (* non cancellare *)\r
if problem_done p then raise Done else p\r
;;\r
\r
+let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
+\r
let ignore var n p =\r
-print_endline (\r
- "--- EAT on " ^ string_of_t p (V var)\r
- ^ " (of:" ^ string_of_int n ^ ")");\r
+ print_cmd "EAT" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
let rec aux m t =\r
if m = 0\r
then lift n t\r
else L (aux (m-1) t) in\r
- let subst = var, aux n (V var) in\r
+ let p, fresh = freshvar p in\r
+ let subst = var, aux n (V fresh) in\r
sanity (subst_in_problem subst p)\r
;;\r
\r
-let explode' var p =\r
- print_endline (\r
- "--- EXPLODE on " ^ string_of_t p (V var)\r
- );\r
- let subst = var, B in\r
- sanity (subst_in_problem subst p)\r
- ;;\r
-\r
let explode p =\r
- match p.div with\r
- | V var -> explode' var p\r
+ let fv1 = List.concat (List.map (visible_vars p) p.div) in\r
+ let fv2 = List.concat (List.map (visible_vars p) p.conv) in\r
+ let fv = List.filter (fun x -> not (List.mem x fv2)) fv1 in\r
+ let fv = List.filter ((<) p.orig_freshno) fv in\r
+ match fv with\r
+ | var::_ ->\r
+ print_cmd "EXPLODE" ("on " ^ string_of_t p (V var));\r
+ let subst = var, B in\r
+ sanity (subst_in_problem subst p)\r
| _ -> problem_fail p "premature explosion"\r
;;\r
\r
let step var p =\r
- print_endline (\r
- "--- STEP on " ^ string_of_t p (V var));\r
+ print_cmd "STEP" ("on " ^ string_of_t p (V var));\r
let subst = var, LM([], 0, var) in\r
sanity (subst_in_problem subst p)\r
;;\r
\r
let id var p =\r
- print_endline (\r
- "--- ID on " ^ string_of_t p (V var));\r
+ print_cmd "ID" ("on " ^ string_of_t p (V var));\r
let subst = var, L(V 0) in\r
sanity (subst_in_problem subst p)\r
;;\r
\r
let apply var appk p =\r
- print_endline (\r
- "--- APPLY_CONSTS on " ^ string_of_t p (V var)\r
- ^ " (special_k:" ^ string_of_int appk ^ ")");\r
+ print_cmd "APPLY"\r
+ (string_of_t p (V var) ^ " applies no." ^ string_of_int appk ^ " fresh variables");\r
let rec mk_freshvars n p =\r
if n = 0\r
then p, []\r
let p, v = freshvar p in\r
p, V(v)::vs in\r
let p, vars = mk_freshvars appk p in\r
- let p, t = mk_apps p (V 0) (List.map (lift 1) vars) in\r
+ let p, t = mk_apps false p (V 0) (List.map (lift 1) vars) in\r
let t = L (A (lift 1 (V var), t)) in\r
let subst = var, t in\r
sanity (subst_in_problem subst p)\r
;;\r
\r
let perm var n p =\r
- print_endline (\r
- "--- PERM on " ^ string_of_t p (V var)\r
- ^ " (of:" ^ string_of_int n ^ ")");\r
- (* let p, v = freshvar p in *)\r
+ print_cmd "PERM" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
+ let p, v = freshvar p in\r
let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in\r
let rec aux m t =\r
if m = 0\r
then aux' (n-1) t\r
else L (aux (m-1) t) in\r
- let t = aux n (lift n (V var)) in\r
+ let t = aux n (lift n (V v)) in\r
let subst = var, t in\r
sanity (subst_in_problem subst p)\r
;;\r
allo stesso modo e' possibile ignorare dei rami se vanno in variabili, e quelle variabili\r
vengono sostituite ovunque: con bombe in conv e con pacman in div\r
*)\r
-(* let forget var n p =\r
- let remove_from_branch p var n = ... in\r
- let p, (tm, c) = remove_from_branch p var n in\r
- print_endline (\r
- "--- FORGET " ^ string_of_t p tm ^ " from the match of " ^ string_of_t p (V var)\r
- ^ " (of:" ^ string_of_int n ^ ")");\r
- sanity p\r
-;; *)\r
+let forget var no p =\r
+ try\r
+ let l = List.assoc var p.matches in\r
+ let (b,(tm,c)) = List.nth l no in\r
+ let l = List.mapi (fun n x -> if n = no then (b,(B,c)) else x) l in\r
+ let matches = List.map (fun (v,lst) -> v, if v = var then l else lst) p.matches in\r
+ let p = {p with matches} in\r
+ print_cmd "FORGET" (string_of_t p tm ^ " from the match of " ^ string_of_t p (V var));\r
+ sanity p\r
+ (* (match c with\r
+ | V var ->\r
+ print_endline (\r
+ "--- FORGET " ^ string_of_t p tm ^ " from the match of " ^ string_of_t p (V var));\r
+ let p = forget_variable var p in\r
+\r
+ | _ -> print_endline "too late to forget that term"; p\r
+ ) *)\r
+ with Failure "nth" ->\r
+ print_endline "wtf?"; p\r
+;;\r
\r
let parse strs =\r
- let dummy_p = {freshno=0; div=V 0; conv=[]; matches=[]; sigma=[]} in\r
+ let dummy_p = {orig_freshno=0; freshno=0; div=[]; conv=[]; matches=[]; sigma=[]} in\r
let rec aux level = function\r
| Parser.Lam t -> L (aux (level + 1) t)\r
| Parser.App (t1, t2) ->\r
- if level = 0 then snd (mk_app dummy_p (aux level t1) (aux level t2))\r
+ if level = 0 then snd (mk_app false dummy_p (aux level t1) (aux level t2))\r
else A(aux level t1, aux level t2)\r
| Parser.Var v -> V v\r
in let (tms, free) = Parser.parse_many strs\r
in (List.map (aux 0) tms, free)\r
;;\r
\r
+let rec list_split n =\r
+ function\r
+ | [] -> [], []\r
+ | x::xs as l -> if n = 0 then [], l else let a, b = list_split (n-1) xs in x::a, b\r
+;;\r
+\r
let magic6 div conv cmds =\r
print_hline ();\r
- let all_tms, var_names = parse (div :: conv) in\r
- let div, conv = List.hd all_tms, List.tl all_tms in\r
- let freshno = 1 + List.length var_names in\r
- let p = {freshno; div; conv; matches=[]; sigma=[]} in\r
+ let all_tms, var_names = parse (div @ conv) in\r
+ let div, conv = list_split (List.length div) all_tms in\r
+ let varno = List.length var_names in\r
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in\r
let p = try\r
let subst = Util.index_of "BOMB" var_names, L B in\r
let p = subst_in_problem subst p in p\r
\r
let interactive div conv cmds =\r
print_hline ();\r
- let all_tms, var_names = parse (div :: conv) in\r
- let div, conv = List.hd all_tms, List.tl all_tms in\r
- let freshno = 1 + List.length var_names in\r
- let p = {freshno; div; conv; matches=[]; sigma=[]} in\r
+ let all_tms, var_names = parse (div @ conv) in\r
+ let div, conv = list_split (List.length div) all_tms in\r
+ let varno = List.length var_names in\r
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in\r
+ (* activate bombs *)\r
let p = try\r
let subst = Util.index_of "BOMB" var_names, L B in\r
- let p = subst_in_problem subst p in p\r
+ subst_in_problem subst p\r
+ with Not_found -> p in\r
+ (* activate pacmans *)\r
+ let p = try\r
+ let subst = Util.index_of "PACMAN" var_names, P in\r
+ let p = subst_in_problem subst p in\r
+ (print_endline ("after subst in problem " ^ string_of_problem p); p)\r
with Not_found -> p in\r
+ (* initial sanity check *)\r
let p = sanity p in\r
let p = List.fold_left (|>) p cmds in\r
let rec f p cmds =\r
else if uno = "step" then step (nth spl 1)\r
else if uno = "perm" then perm (nth spl 1) (nth spl 2)\r
else if uno = "apply" then apply (nth spl 1) (nth spl 2)\r
+ else if uno = "forget" then forget (nth spl 1) (nth spl 2)\r
else if uno = "id" then id (nth spl 1)\r
- else failwith "unknown"\r
- with Failure _ -> print_endline "Wrong input."; (fun x -> x) in\r
+ else failwith "Wrong input."\r
+ with Failure s -> print_endline s; (fun x -> x) in\r
let str, cmd = read_cmd () in\r
- let cmds = str::cmds in\r
+ let cmds = (" " ^ str ^ ";")::cmds in\r
try\r
let p = cmd p in f p cmds\r
with\r
- | Done -> List.iter print_endline (List.rev cmds)\r
+ | Done -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
in f p []\r
;;\r
\r
let _ = magic6\r
- "x x"\r
+ ["x x"]\r
[ "_. BOMB" ]\r
[ ignore 1 1; explode ]\r
;;\r
\r
let _ = magic6\r
- "x y BOMB b"\r
+ ["x y BOMB b"]\r
[ "x BOMB y c" ]\r
- [ perm 1 3; step 1 ; ignore 8 2; explode; ];;\r
+ [ perm 1 3; step 8 ; explode; ];;\r
\r
let _ = magic6\r
- "x BOMB a1 c"\r
+ ["x BOMB a1 c"]\r
[ "x y BOMB d"; "x BOMB a2 c" ]\r
- [ perm 1 3 ; step 1 ; step 12; ignore 13 1; explode; ]\r
+ [ perm 1 3 ; step 10 ; step 13; explode; ]\r
;;\r
\r
let _ = magic6\r
- "x (x x)"\r
+ ["x (x x)"]\r
[ "x x" ; "x x x" ] [\r
apply 1 1;\r
step 1;\r
];;\r
\r
let _ = magic6\r
- "x (_.BOMB)"\r
+ ["x (_.BOMB)"]\r
[ "x (_._. BOMB)" ]\r
[ apply 1 2; ]\r
;;\r
\r
let _ = magic6\r
- "x (_.y)"\r
+ ["x (_.y)"]\r
[ "y (_. x)" ]\r
[ apply 1 1; ignore 1 1; explode; ]\r
;;\r
\r
let _ = magic6\r
- "y (x a1 BOMB c) (x BOMB b1 d)"\r
+ ["y (x a1 BOMB c) (x BOMB b1 d)"]\r
[ "y (x a2 BOMB c) (x BOMB b1 d)";\r
- "y (x a1 BOMB c) (x BOMB b2 d)";]\r
- [ 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
+ "y (x a1 BOMB c) (x BOMB b2 d)";] [\r
+ perm 2 3;\r
+ step 12;\r
+ perm 17 2;\r
+ step 19;\r
+ step 18;\r
+ ignore 22 1;\r
+ ignore 21 1;\r
+ ignore 24 1;\r
+ ignore 25 1;\r
+ step 1;\r
+ step 32;\r
+ explode;\r
+ ]\r
;;\r
\r
let _ = magic6\r
- "z (y x)"\r
+ ["z (y x)"]\r
[ "z (y (x.x))"; "y (_. BOMB)" ]\r
- [ apply 2 1; step 3; explode' 8; ]\r
+ [ apply 2 1; step 3; explode; ]\r
;;\r
\r
let _ = magic6\r
- "y x"\r
+ ["y x"]\r
[ "y (x.x)"; "x (_. BOMB)" ]\r
[ apply 1 1; ignore 2 1; step 1; explode; ]\r
;;\r
\r
let _ = magic6\r
- "z (y x)"\r
+ ["z (y x)"]\r
[ "z (y (x.x))"; "y (_. BOMB)" ]\r
[ step 1; explode; apply 2 1; id 2; ignore 3 1; ]\r
;;\r
\r
let _ = magic6\r
- "y (x a)"\r
+ ["y (x a)"]\r
[ "y (x b)"; "x BOMB" ] [\r
id 2;\r
step 1;\r
];;\r
\r
magic6\r
- "y (x a)" [ "y (x b)"; "x BOMB"; "y a" ]\r
+ ["y (x a)"] [ "y (x b)"; "x BOMB"; "y a" ]\r
[\r
apply 1 1;\r
perm 2 2;\r
- perm 2 2;\r
- step 3;\r
- apply 2 1;\r
- ignore 4 1;\r
- step 2;\r
- ignore 12 1;\r
- ignore 13 1;\r
- step 1;\r
+ ignore 9 1;\r
+ step 10;\r
explode;\r
+ ];;\r
+(* "y (a c)"\r
+[ "y (b c)"; "y (x a)"; "y (x b)"; "x BOMB" ] *)\r
+\r
+magic6\r
+["x a (x (a.y BOMB))"]\r
+[ "x b"; "x (y c)"; "x (y d)" ]\r
+[apply 1 1;\r
+apply 2 1;\r
+explode;]\r
+(* [\r
+step 1;\r
+step 3;\r
+explode' 10;\r
+(* ma si puo' fare anche senza forget *) *)\r
+(* ] *)\r
+;;\r
+\r
+(* dipendente dalla codifica? no, ma si risolve solo con id *)\r
+magic6\r
+ ["y a"] ["y b"; "x (y (_.BOMB))"]\r
+[\r
+apply 1 1;\r
+apply 2 1;\r
+explode;\r
];;\r
+ (* [id 1; explode];; *)\r
\r
-interactive\r
- "y (x a)"\r
-[ "y (x b)"; "x BOMB"; "y a" ] [];;\r
+magic6\r
+ ["PACMAN (x x x)"] ["PACMAN (x x)"]\r
+ [\r
+ ignore 2 2;\r
+ explode;\r
+ ];;\r
\r
+print_hline();\r
print_endline "ALL DONE. "\r
projects / fireball-separation.git / blobdiff