+++ /dev/null
-type var = (* unique name *) int * (int * term) option * (*level*) int\r
-and term =\r
- | Tvar of var\r
- | Tapp of term * term\r
- | Tlam of int * term\r
-;;\r
-\r
-let zero = Tvar(1010, None, 0);;\r
-let dummy = Tvar(333, None, 0);;\r
-\r
-(* mk_app & subst implementano la beta *)\r
-let rec mk_app t1 t2 = match t1 with\r
- | Tlam(v, t1') -> subst v t2 t1'\r
- | _ -> Tapp(t1, t2)\r
-and subst v tv =\r
- let rec aux = function\r
- | Tapp(t1, t2) -> mk_app (aux t1) (aux t2)\r
- | Tvar(v', _, _) as t -> if v = v' then tv else t\r
- | Tlam(v', t') as t -> if v = v' then t else Tlam(v', aux t')\r
- in aux\r
-;;\r
-\r
-(* PARSING AND PRINTING *)\r
-\r
-let parse =\r
- let rec minus1 = function\r
- | Tvar(n, None, x) -> Tvar(n-1, None, x)\r
- | Tvar _ -> assert false\r
- | Tapp(t1, t2) -> Tapp(minus1 t1, minus1 t2)\r
- | Tlam(n, t) -> Tlam(n-1, minus1 t)\r
- (* in let open Parser *)\r
- in let rec myterm_of_term = function\r
- | Parser.Var n -> Tvar(n, None, 0)\r
- | Parser.App(t1, t2) -> (*Tapp(myterm_of_term t1, myterm_of_term t2) WARNING! BETA DOWN HERE! *)\r
- mk_app (myterm_of_term t1) (myterm_of_term t2)\r
- | Parser.Lam(t) -> minus1 (Tlam(0, myterm_of_term t))\r
- in fun strs -> (\r
- let (tms, free) = Parser.parse_many strs\r
- in List.map myterm_of_term tms\r
- )\r
-;;\r
-\r
-(* PRETTY PRINTING *)\r
-open Console;;\r
-\r
-let fancy_of_term t =\r
-let rec string_of_term =\r
- let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"] in\r
- let bound = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in\r
- let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in\r
- let rec string_of_var t =\r
- if Tvar t = dummy then "_" else if Tvar t = zero then "ZZ" else match t with\r
- | (n, None, _) -> (string_of_int' n)\r
- (* | (_, Some(n,t), _) -> "?" ^ string_of_int n *)\r
- | (_, Some(n,t), _) -> "{" ^ (string_of_term_no_pars t) ^ "|" ^ (string_of_int n) ^ "}"\r
- and string_of_term_w_pars = function\r
- | Tvar v -> string_of_var v\r
- | Tapp(t1, t2) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"\r
- | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"\r
- and string_of_term_no_pars_app = function\r
- | Tapp(t1, t2) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)\r
- | _ as t -> string_of_term_w_pars t\r
- and string_of_term_no_pars_lam = function\r
- | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)\r
- | _ as t -> string_of_term_no_pars t\r
- and string_of_term_no_pars = function\r
- | Tlam(_, _) as t -> string_of_term_no_pars_lam t\r
- | _ as t -> string_of_term_no_pars_app t\r
- in string_of_term_no_pars\r
-in let rec html_of_term =\r
- let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"] in\r
- let bound = ["x"; "y"; "z"; "w"; "q"] in\r
- let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in\r
- let rec string_of_var t =\r
- if Tvar t = dummy then "#" else if Tvar t = zero then "Z" else match t with\r
- | (n, None, _) -> (string_of_int' n)\r
- | (_, Some(n,t), _) -> "α<sup>" ^ (string_of_term_no_pars t) ^ "</sup><sub>" ^ (string_of_int n) ^ "</sub>"\r
- and string_of_term_w_pars = function\r
- | Tvar v -> string_of_var v\r
- | Tapp(t1, t2) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"\r
- | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"\r
- and string_of_term_no_pars_app = function\r
- | Tapp(t1, t2) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)\r
- | _ as t -> string_of_term_w_pars t\r
- and string_of_term_no_pars_lam = function\r
- | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)\r
- | _ as t -> string_of_term_no_pars t\r
- and string_of_term_no_pars = function\r
- | Tlam(_, _) as t -> string_of_term_no_pars_lam t\r
- | _ as t -> string_of_term_no_pars_app t\r
- in string_of_term_no_pars\r
-in\r
- string_of_term t / html_of_term t\r
-;;\r
-\r
-let fancy_of_nf t: Console.fancyobj =\r
-let rec print ?(l=[]) =\r
- function\r
- `Var n -> Lambda3.print_name l n\r
- | `N n -> string_of_int n\r
- | `Match(t,bs_lift,bs,args) ->\r
- "([" ^ print ~l (t :> Lambda3.nf) ^\r
- " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (Lambda3.lift bs_lift t)) !bs) ^ "] " ^\r
- String.concat " " (List.map (print ~l) args) ^ ")"\r
- | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"\r
- | `Lam nf ->\r
- let name = Lambda3.string_of_var (List.length l) in\r
- "" ^ name ^ "." ^ print ~l:(name::l) (nf : Lambda3.nf)\r
-\r
-in let rec print_html ?(l=[]) =\r
- function\r
- `Var n -> Lambda3.print_name l n\r
- | `N n -> string_of_int n\r
- | `Match(t,bs_lift,bs,args) ->\r
- "(<b>match</b> " ^ print_html ~l (t :> Lambda3.nf) ^\r
- " <b>with</b> " ^ String.concat " <b>|</b> " (List.map (fun (n,t) -> string_of_int n ^ " <b>⇒</b> " ^ print_html ~l (Lambda3.lift bs_lift t)) !bs) ^ "..." (* Attenzion non sto stampando gli argomenti applicati! Perche' non ce ne sono mai *)\r
- | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print_html ~l) args)) ^ ")"\r
- | `Lam nf ->\r
- let name = Lambda3.string_of_var (List.length l) in\r
- "λ" ^ name ^ ". " ^ print_html ~l:(name::l) (nf : Lambda3.nf)\r
-in\r
- print t / print_html t\r
-;;\r
-\r
-let print_term t = print_endline (fancy_of_term t :> Console.fancyobj);;\r
-(* *)\r
-\r
-\r
-let varcount = ref 0;;\r
-\r
-let freshvar () = (\r
- varcount := (!varcount + 1);\r
- !varcount\r
-);;\r
-\r
-let rec hd =\r
- function\r
- | Tvar x -> x\r
- | Tapp(t1,t2) -> hd t1\r
- | Tlam _ -> assert false\r
-;;\r
-\r
-let alive (_, _, n) = n;;\r
-let rec setalive c = function\r
- | Tvar(a,b,_) as v -> if v <> zero && v <> dummy then Tvar(a,b,c) else v\r
- | Tapp(a,b) -> Tapp(setalive c a, setalive c b)\r
- | Tlam(n, t) -> Tlam(n, setalive c t)\r
-;;\r
-\r
-let mk_vars t lev =\r
- let rec aux n =\r
- if n = 0\r
- then []\r
- else Tvar(0, Some(n, t), lev) :: (aux (n-1))\r
- in aux\r
-;;\r
-\r
-let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)\r
-\r
-\r
-let compute_special_k tms =\r
- let rec aux k t = match t with\r
- | Tvar _ -> 0\r
- | Tapp(t1,t2) -> Pervasives.max (aux 0 t1) (aux 0 t2)\r
- | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)\r
- in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms\r
-;;\r
-\r
-let compute_special_h tms =\r
- let rec eat_lam = function\r
- | Tlam(_,t) -> eat_lam t\r
- | _ as t -> t\r
- in\r
- let rec aux t = match t with\r
- | Tvar _ -> 0\r
- | Tapp(t1,t2) -> Pervasives.max (aux t1) (aux t2)\r
- | Tlam(v,t) -> 1 + (aux (eat_lam t))\r
- in 1 + List.fold_left (fun b a -> Pervasives.max (aux a) b) 0 tms\r
-;;\r
-\r
-(* funzione di traduzione brutta & cattiva *)\r
-let translate k =\r
- let rec aux = function\r
- | Tlam _ -> assert false\r
- | Tvar _ as v -> v\r
- | Tapp(t1, t2) ->\r
- let v = hd t1 in\r
- let a = alive v in\r
- let t1' = aux t1 in\r
- let t2' = if a = 0\r
- then t2\r
- else mk_apps t2 ((List.rev (mk_vars t1' (a-1) k)) @ [zero])\r
- in Tapp(t1', aux t2')\r
- in aux\r
-;;\r
-\r
-(* sostituisce gli argomenti dummy (delle variabili morte) con 'dummy' *)\r
-let rec dummize = function\r
- | Tlam _ -> assert false\r
- | Tvar (a,Some(b,t), c) -> Tvar(a, Some (b, dummize t), c)\r
- | Tvar _ as v -> v\r
- | Tapp(t1, t2) ->\r
- if alive (hd t1) = 0\r
- then Tapp(dummize t1, dummy)\r
- else Tapp(dummize t1, dummize t2)\r
-;;\r
-\r
-(* lista di sottotermini applicativi *)\r
-let rec subterms = function\r
- | Tlam _ -> assert false\r
- | Tvar _ as v -> [v]\r
- | Tapp(t1, t2) -> Tapp(t1, t2) :: ((subterms t1) @ (subterms t2))\r
-;;\r
-\r
-(* filtra dai sottotermini le variabili *)\r
-let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;\r
-\r
-\r
-let rec stupid_uniq = function\r
- | [] -> []\r
- | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)\r
-;;\r
-let stupid_compare a b =\r
- let rec size = function\r
- | Tvar(_,None,_) -> 0\r
- | Tvar(_,Some(_,t),_) -> 1 + size t\r
- | Tapp(t1,t2) -> 1 + size t1 + size t2\r
- | Tlam _ -> assert false\r
- in compare (size a) (size b)\r
-;;\r
-let stupid_sort_uniq l = stupid_uniq (List.sort stupid_compare l);;\r
-\r
-(* crea i match ricorsivamente.\r
- - k e' lo special-K\r
- - subs e' l'insieme dei sottotermini\r
- TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione\r
- *)\r
-let crea_match k subs (acc : (term * Lambda3.nf) list) : term -> Lambda3.nf =\r
- let req t = try List.assoc t acc with Not_found -> `Var 9999 in\r
- let aux t1 = (\r
- if t1 = dummy then `Var 99999 else\r
- (* let _ = print_term t1 in *)\r
- let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2)) subs) subs\r
- in if cont = [] then\r
- try `N (Lambda3.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else\r
- let a = alive (hd t1) in\r
- if a = 0 then `Lam (req (Tapp(t1, dummy)))\r
- else (\r
- let vars = (List.rev (mk_vars t1 (a-1) k)) @ [zero]\r
- (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))\r
- in let _ = print_term (mk_apps dummy vars) *)\r
- in let vars = List.map req vars\r
- in let vars = List.map (Lambda3.lift 1) vars (* forse lift non necessario *)\r
- in let vars = Listx.from_list vars\r
- in let body = `I(0, vars)\r
- in let branches = List.map (fun t2 -> (Lambda3.index_of t2 subs, req (Tapp(t1, t2)))) cont\r
- in let bs = ref(branches)\r
- in let lift = 1\r
- in let args = []\r
- in `Lam (`Match(body, lift, bs, args))\r
- )\r
- ) in aux\r
-;;\r
-\r
-let mk_zeros k =\r
- let rec aux n prev =\r
- if n = 0 then [zero]\r
- else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev\r
- in aux (k+1) []\r
-;;\r
-\r
-let is_scott_n t n =\r
- let open Lambda3 in let open Pure in\r
- let rec aux n = function\r
- | L (L (A (V 1, L (V 0)))) -> n = 0\r
- | L (L (A (V 0, t))) -> aux (n-1) t\r
- | _ -> assert false\r
- in aux n t\r
-;;\r
-\r
-(* do the magic *)\r
-let magic strings k h = (\r
- let tms = parse strings\r
- in let tms = List.map (fun x -> Tapp(x, zero)) tms\r
- in let tms' = List.map (setalive h) tms\r
- in let tms' = List.map (translate k) tms'\r
- in let tms' = List.map dummize tms'\r
- in let progress s = print_bullet (fancy_of_string s)\r
- in let _ = progress "traduzione completata"\r
- (* in let _ = List.map print_term tms' *)\r
- in let _ = progress "ordino i sottotermini"\r
- in let subs = List.concat (List.map subterms tms')\r
- in let subs = stupid_sort_uniq subs\r
- (* metti gli zeri in testa, perche' vanno calcolati per primi *)\r
- in let zeros = mk_zeros k\r
- in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)\r
- in let _ = progress ("sottotermini generati: " ^ string_of_int (List.length subs))\r
- in let vars = vars subs\r
- (* in let _ = List.iter print_term subs *)\r
- (* in let _ = 0/0 *)\r
- in let fv = List.filter (function Tvar(_, None, _) as v -> v <> dummy | _ -> false) vars\r
- (* in let _ = print_string ("> free vars: " ^ String.concat ", " (List.map (string_of_term) fv)) *)\r
- in let _ = progress "sto creando i match"\r
- (* in let sigma = List.map (fun x -> x, crea_match k subs x) fv *)\r
- in let f t acc = let res = crea_match k subs acc t in (t,res)::acc\r
- in let acc = List.fold_right f subs []\r
- in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc\r
- in let _ = progress "match creati"\r
- in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " ↦ ") ^^ fancy_of_nf y)) sigma\r
-\r
- in let _ = progress "controllo di purezza";\r
- in let open Lambda3\r
- in let ps, _ = Lambda3.parse' strings\r
- in let ps = List.map (fun x -> Lambda3.mk_app x (`Var 1010)) ps\r
- in let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) ps\r
- in let sigma = List.map (\r
- function (Tvar(n,_,_), inst) -> n, ToScott.t_of_nf inst | _ -> assert false\r
- ) sigma\r
- in let ps =\r
- List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma\r
- in let _ = List.iteri (fun i n ->\r
- (* print_string_endline ((string_of_int i) ^ ":: " ^ (Pure.print (Pure.whd n))); *)\r
- (* assert (Pure.whd n = Scott.mk_n (Lambda3.index_of (List.nth tms' i) subs))) ps *)\r
- assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs))) ps\r
- in let _ = progress "fatto." in ()\r
-);;\r
-\r
-let do_everything tms =\r
-let tms' = parse tms in\r
-let _ = List.iter print_term tms' in\r
-let k = compute_special_k tms' in\r
-let h = compute_special_h tms' in\r
-(* let _ = print_string_endline (string_of_int h) in *)\r
-magic tms k h\r
-;;\r
-\r
-let _ =\r
- let tms = ["a a"; "a b"; "b a"; "b (x. y.x y a)"] in\r
- (* 1 2 *)\r
- (* let tms = ["x c" ; "b (x c d e)"; "b"] in *)\r
- (* 0 1 *)\r
- (* let tms = ["x x x"] in *)\r
- let tms' = parse tms in\r
- let _ = List.iter print_term tms' in\r
- let k = compute_special_k tms' in\r
- let h = compute_special_h tms' in\r
- (* let _ = print_string_endline (string_of_int h) in *)\r
- magic tms k h\r
-;;\r
-\r
-(* type var' = (* unique name *) int * (int * term') option * (*dead*) bool option\r
-and term' =\r
- | Tvar' of var'\r
- | Tapp' of term' * term' * (* active *) bool\r
- | Tlam' of int * term'\r
-;;\r
-\r
-let rec iter mustapply =\r
- let aux = function\r
- | Tvar'(n, Some(m,t), b) -> Tvar(n, Some(m, aux t), b)\r
- | Tvar' _ as v -> v\r
- | Tapp'(t1, t2, b) -> if b &&\r
- in aux\r
-;; *)\r
+++ /dev/null
-let print_hline = Console.print_hline;;\r
-\r
-type var = int;;\r
-\r
-type t =\r
- | V of var\r
- | A of t * t\r
- | L of t\r
- | LM of\r
- t list (* body of the match *)\r
- * int (* explicit liftno *)\r
- * int (* variable which originated this match (id) *)\r
- | B (* bottom *)\r
- | P (* pacman *)\r
-;;\r
-\r
-\r
-type problem = {\r
- freshno : int\r
- ; div : t\r
- ; conv : t list\r
- ; matches : (var (* variable originating this match *) * (t (* term to discriminate *) * t (* continuation *)) list) list\r
- ; sigma : (var * t) list (* substitutions *)\r
-}\r
-\r
-let string_of_t p =\r
- let bound_vars = ["x"; "y"; "z"; "z1"; "z2"] in\r
- let rec aux level = function\r
- | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)\r
- | A (t1,t2) -> "("^aux level t1^" "^aux level t2^")"\r
- | L t -> "(\\" ^ aux (level+1) (V 0) ^ ". " ^ aux (level+1) t ^ ")"\r
- | LM (ts,liftno,id) -> "[match orig="^aux 0 (V id)^"]"\r
- | B -> "BOT"\r
- | P -> "PAC"\r
- in aux 0\r
-;;\r
-\r
-let string_of_problem p =\r
- let lines = [\r
- "[DV] " ^ 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
- (* ^" -> " ^ 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 (string_of_problem p);\r
- failwith reason\r
-;;\r
-\r
-let freshvar ({freshno} as p) =\r
- {p with freshno=freshno+1}, freshno+1\r
-;;\r
-\r
-let add_to_match p id entry =\r
- let matches = try\r
- let _ = List.assoc id p.matches in\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
-;;\r
-\r
-let free_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
- | L t -> aux (level+1) t\r
- | LM(ts,_,_) -> List.fold_left (fun a b -> a || aux (level+1) b) false ts\r
- | B -> false\r
- | P -> false\r
- in aux 0\r
-;;\r
-\r
-let rec is_inert =\r
- function\r
- | A(t,_) -> is_inert t\r
- | L _ | LM _ | B -> false\r
- | _ -> true\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
- 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
- | 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
- 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
- | 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
- 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
- | 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
- | LM(ts,liftno,id) ->\r
- let p, t = mk_apps 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
- p, newvar\r
- | B\r
- | _ when t2 = B -> p, B\r
- | t1 -> p, A (t1, t2)\r
-and mk_apps 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
- ;;\r
-\r
-let subst = subst 0 false;;\r
-\r
-let mk_lambda t = L (lift 1 t) ;;\r
-\r
-let subst_many sub =\r
- let rec aux p = function\r
- | [] -> p, []\r
- | t::tms ->\r
- let p, t = subst sub p t in\r
- let p, tms = aux p tms in\r
- p, t :: tms\r
- in aux\r
-;;\r
-\r
-let rec subst_in_matches sub p =\r
- function\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 branches = List.combine a b in\r
- let p, ms = subst_in_matches sub p ms in\r
- p, (v, branches) :: ms\r
-;;\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 p, matches = subst_in_matches sub p p.matches in\r
- {p with div=div; conv=conv; matches=matches; sigma=sub::p.sigma}\r
-;;\r
-\r
-(* FIXME *)\r
-let unify_terms p t1 t2 =\r
- match t1 with\r
- | V v -> subst_in_problem (v, t2) p\r
- | _ -> problem_fail p "The collapse of a match came after too many steps :(";;\r
-\r
-let rec unify p =\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
- let rec aux = function\r
- | [] -> [], None\r
- | (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
- ) in\r
- function\r
- | [] -> [], None\r
- | (orig,branches) :: ms ->\r
- match aux branches with\r
- | _, None -> let ms, res = give_duplicates ms in (orig,branches) :: ms, res\r
- | branches', Some subst -> (orig,branches') :: ms, Some subst in\r
- let matches, vars_to_be_unified = give_duplicates p.matches in\r
- let p = {p with matches=matches} in\r
- match vars_to_be_unified with\r
- | None -> p\r
- | Some(t', t) ->\r
- (* print_endline ("> unify " ^ string_of_t p (t') ^ " with " ^ string_of_t p t); *)\r
- unify (unify_terms p t' t)\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
-;;\r
-\r
-exception Done;;\r
-\r
-let sanity p =\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
-\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
- if problem_done p then raise Done else p\r
-;;\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
- 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
- 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
- | _ -> 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
- 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
- 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
- let rec mk_freshvars n p =\r
- if n = 0\r
- then p, []\r
- else\r
- let p, vs = mk_freshvars (n-1) p in\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 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
- 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 subst = var, t in\r
- sanity (subst_in_problem subst p)\r
-;;\r
-\r
-(* TODO:\r
-- cosi' come e' possibile unificare rami di branch solo se vanno -> a variabili,\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
-\r
-let parse strs =\r
- let dummy_p = {freshno=0; div=V 0; 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
- 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 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 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
- with Not_found -> p in\r
- let p = sanity p in\r
- try\r
- problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
- with\r
- | Done -> ()\r
-;;\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 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
- with Not_found -> p in\r
- let p = sanity p in\r
- let p = List.fold_left (|>) p cmds in\r
- let rec f p cmds =\r
- let nth spl n = int_of_string (List.nth spl n) in\r
- let read_cmd () =\r
- let s = read_line () in\r
- let spl = Str.split (Str.regexp " +") s in\r
- s, let uno = List.hd spl in\r
- try if uno = "explode" then explode\r
- else if uno = "ignore" then ignore (nth spl 1) (nth spl 2)\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 = "id" then id (nth spl 1)\r
- else failwith "unknown"\r
- with Failure _ -> print_endline "Wrong input."; (fun x -> x) in\r
- let str, cmd = read_cmd () 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
- in f p []\r
-;;\r
-\r
-let _ = magic6\r
- "x x"\r
- [ "_. BOMB" ]\r
- [ ignore 1 1; explode ]\r
-;;\r
-\r
- let _ = magic6\r
- "x y BOMB b"\r
- [ "x BOMB y c" ]\r
- [ perm 1 3; step 1 ; ignore 8 2; explode; ];;\r
-\r
-let _ = magic6\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
-;;\r
-\r
-let _ = magic6\r
- "x (x x)"\r
- [ "x x" ; "x x x" ] [\r
- apply 1 1;\r
- step 1;\r
- explode;\r
- step 9;\r
-];;\r
-\r
-let _ = magic6\r
- "x (_.BOMB)"\r
- [ "x (_._. BOMB)" ]\r
- [ apply 1 2; ]\r
-;;\r
-\r
-let _ = magic6\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 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
-;;\r
-\r
-let _ = magic6\r
- "z (y x)"\r
- [ "z (y (x.x))"; "y (_. BOMB)" ]\r
- [ apply 2 1; step 3; explode' 8; ]\r
-;;\r
-\r
-let _ = magic6\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.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 b)"; "x BOMB" ] [\r
- id 2;\r
- step 1;\r
- explode;\r
-];;\r
-\r
-magic6\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
- explode;\r
-];;\r
-\r
-interactive\r
- "y (x a)"\r
-[ "y (x b)"; "x BOMB"; "y a" ] [];;\r
-\r
-print_endline "ALL DONE. "\r
projects / fireball-separation.git / commitdiff