ocaml/andrea4.ml

   1 (* type var = (* unique name *) int * (int * term) option * (*level*) int *)\r
   2 type term =\r
   3   | Tvar of int\r
   4   | Tapp of term * term * bool\r
   5   | Tlam of int * term\r
   6 ;;\r
   7 \r
   8 let zero = Tvar 1010;;\r
   9 let dummy = Tvar 333;;\r
  10 \r
  11 \r
  12 (* mk_app & subst implementano la beta *)\r
  13 let rec mk_app t1 t2 = match t1 with\r
  14   | Tlam(v, t1') -> subst v t2 t1'\r
  15   | _ -> Tapp(t1, t2, false)\r
  16 and subst v tv =\r
  17   let rec aux = function\r
  18   | Tapp(t1, t2, _) -> mk_app (aux t1) (aux t2)\r
  19   | Tvar v' as t -> if v = v' then tv else t\r
  20   | Tlam(v', t') as t -> if v = v' then t else Tlam(v', aux t')\r
  21   in aux\r
  22 ;;\r
  23 \r
  24 (* PARSING AND PRINTING *)\r
  25 \r
  26 let parse =\r
  27   let rec minus1 = function\r
  28     | Tvar n -> Tvar (n-1)\r
  29     | Tapp(t1, t2, b) -> Tapp(minus1 t1, minus1 t2, b)\r
  30     | Tlam(n, t) -> Tlam(n-1, minus1 t)\r
  31   (* in let open Parser *)\r
  32   in let rec myterm_of_term = function\r
  33     | Parser.Var n -> Tvar n\r
  34     | Parser.App(t1, t2) -> (*Tapp(myterm_of_term t1, myterm_of_term t2) WARNING! BETA DOWN HERE! *)\r
  35                             mk_app (myterm_of_term t1) (myterm_of_term t2)\r
  36     | Parser.Lam(t) -> minus1 (Tlam(0, myterm_of_term t))\r
  37   in fun strs -> (\r
  38     let (tms, free) = Parser.parse_many strs\r
  39     in List.map myterm_of_term tms\r
  40     )\r
  41 ;;\r
  42 \r
  43 (* PRETTY PRINTING *)\r
  44 open Console;;\r
  45 \r
  46 let fancy_of_term t =\r
  47 let rec string_of_term =\r
  48   let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"] in\r
  49   let bound = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in\r
  50   let string_of_int' n = if n >= 0 then "free" ^ string_of_int n else "bound" ^ string_of_int n  in\r
  51   let rec string_of_var t =\r
  52     if Tvar t = dummy then "_" else if Tvar t = zero then "ZZ" else match t with\r
  53     | n -> string_of_int' n\r
  54   and string_of_term_w_pars = function\r
  55     | Tvar v -> string_of_var v\r
  56     | Tapp(t1, t2, _) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"\r
  57     | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"\r
  58   and string_of_term_no_pars_app = function\r
  59     | Tapp(t1, t2,_) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)\r
  60     | _ as t -> string_of_term_w_pars t\r
  61   and string_of_term_no_pars_lam = function\r
  62     | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)\r
  63     | _ as t -> string_of_term_no_pars t\r
  64   and string_of_term_no_pars = function\r
  65     | Tlam(_, _) as t -> string_of_term_no_pars_lam t\r
  66     | _ as t -> string_of_term_no_pars_app t\r
  67   in string_of_term_no_pars\r
  68 in let rec html_of_term =\r
  69   let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"] in\r
  70   let bound = ["x"; "y"; "z"; "w"; "q"] in\r
  71   let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in\r
  72   let rec string_of_var t =\r
  73     if Tvar t = dummy then "&num;" else if Tvar t = zero then "Z" else string_of_int' t\r
  74   and string_of_term_w_pars = function\r
  75     | Tvar v -> string_of_var v\r
  76     | Tapp(t1, t2,_) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"\r
  77     | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"\r
  78   and string_of_term_no_pars_app = function\r
  79     | Tapp(t1, t2,_) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)\r
  80     | _ as t -> string_of_term_w_pars t\r
  81   and string_of_term_no_pars_lam = function\r
  82     | Tlam(v, t) -> "&lambda;" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)\r
  83     | _ as t -> string_of_term_no_pars t\r
  84   and string_of_term_no_pars = function\r
  85     | Tlam(_, _) as t -> string_of_term_no_pars_lam t\r
  86     | _ as t -> string_of_term_no_pars_app t\r
  87   in string_of_term_no_pars\r
  88 in\r
  89   string_of_term t / "html_of_term t"\r
  90 ;;\r
  91 \r
  92 let fancy_of_nf t: Console.fancyobj =\r
  93 let rec print ?(l=[]) =\r
  94  function\r
  95     `Var n -> Util.Vars.print_name l n\r
  96   | `N n -> string_of_int n\r
  97   | `Match(t,bs_lift,bs,args) ->\r
  98      "([" ^ print ~l (t :> Num.nf) ^\r
  99      " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (Num.lift bs_lift t)) !bs) ^ "] " ^\r
 100      String.concat " " (List.map (print ~l) args) ^ ")"\r
 101   | `I(n,args) -> "(" ^ Util.Vars.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"\r
 102   | `Lam(_,nf) ->\r
 103      let name = Util.Vars.string_of_var (List.length l) in\r
 104      "" ^ name ^ "." ^ print ~l:(name::l) (nf : Num.nf)\r
 105 \r
 106 (* in let rec print_html ?(l=[]) =\r
 107  function\r
 108     `Var n -> Lambda3.print_name l n\r
 109   | `N n -> string_of_int n\r
 110   | `Match(t,bs_lift,bs,args) ->\r
 111      "(<b>match</b> " ^ print_html ~l (t :> Lambda3.nf) ^\r
 112      " <b>with</b> " ^ String.concat " <b>|</b> " (List.map (fun (n,t) -> string_of_int n ^ " <b>&rArr;</b> " ^ print_html ~l (Lambda3.lift bs_lift t)) !bs) ^ "..." (* Attenzion non sto stampando gli argomenti applicati! Perche' non ce ne sono mai *)\r
 113   | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print_html ~l) args)) ^ ")"\r
 114   | `Lam nf ->\r
 115      let name = Lambda3.string_of_var (List.length l) in\r
 116      "&lambda;" ^ name ^ ". " ^ print_html ~l:(name::l) (nf : Lambda3.nf) *)\r
 117 in\r
 118   print t / print t\r
 119 ;;\r
 120 \r
 121 let print_term t = print_endline (fancy_of_term t :> Console.fancyobj);;\r
 122 (*  *)\r
 123 \r
 124 \r
 125 let varcount = ref 11;;\r
 126 \r
 127 let freshvar () = (\r
 128   varcount := (!varcount + 1);\r
 129   !varcount\r
 130 );;\r
 131 \r
 132 let find_applicative =\r
 133   let rec aux = function\r
 134   | Tapp(t1, Tlam _, _) -> Some t1\r
 135   | Tapp(t1, t2, _) ->\r
 136     (match aux t1 with\r
 137     | None -> aux t2\r
 138     | _ as r -> r)\r
 139   | _-> None\r
 140   in let rec aux2 = function\r
 141     | [] -> None\r
 142     | x::xs -> (match aux x with\r
 143       | None -> aux2 xs\r
 144       | _ as result -> result\r
 145     )\r
 146   in aux2\r
 147 ;;\r
 148 \r
 149 let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)\r
 150 \r
 151 let rec hd = function | Tvar _ as x -> x | Tapp(t, _, _) -> hd t | _ -> assert false;;\r
 152 \r
 153 let rec set_applied =\r
 154   function\r
 155   | Tvar _ as v -> v\r
 156   | Tlam _ -> assert false\r
 157   | Tapp(t1,t2,_) -> Tapp(set_applied t1, set_applied t2, true)\r
 158 ;;\r
 159 \r
 160 let rec constant a n =\r
 161   if n = 0 then [] else a:: (constant a (n-1))\r
 162 ;;\r
 163 \r
 164 let rec mk_dummies k t =\r
 165   set_applied (mk_apps t (constant dummy (k+1)))\r
 166 ;;\r
 167 \r
 168 let rec make_lambda_zero k =\r
 169   if k = 0 then mk_dummies (k+1) zero else Tlam(0, make_lambda_zero (k-1))\r
 170 ;;\r
 171 \r
 172 let mk_vars n =\r
 173   let rec aux n =\r
 174     if n = 0\r
 175     then []\r
 176     else (Tvar (freshvar ())) :: (aux (n-1))\r
 177   in aux n @ [make_lambda_zero (n+1)]\r
 178 ;;\r
 179 \r
 180 let apply a vars =\r
 181   let rec aux = function\r
 182   | Tapp(t1, t2, b) ->\r
 183     if t1 = a\r
 184     then (assert (not b); Tapp(aux t1, mk_apps' t2 vars, true))\r
 185     else Tapp(aux t1, aux t2, b)\r
 186   | _ as t -> t\r
 187   and mk_apps' t vars =\r
 188     if t = zero\r
 189     then mk_dummies (List.length vars - 1) t\r
 190     else aux (mk_apps t vars)\r
 191   in aux\r
 192 ;;\r
 193 \r
 194 let round k (app_map, tms) =\r
 195   match find_applicative tms with\r
 196   | None -> raise Not_found\r
 197   | Some a ->\r
 198     let vars = mk_vars k in\r
 199     let f = apply a vars in\r
 200     let app_map = (a, vars) :: (List.map (fun (x,y) -> f x, y) app_map)\r
 201     in (app_map, List.map f tms)\r
 202 ;;\r
 203 \r
 204 let ends_with t1 t2 = match t1 with\r
 205   | Tapp(_, t, _) -> t = t2\r
 206   | _ -> false\r
 207 ;;\r
 208 \r
 209 let rec last_round k (app_map, forbidden, t) =\r
 210   let mk_apps' forbidden t vars =\r
 211     if List.mem t forbidden\r
 212     then mk_dummies (List.length vars - 1) t\r
 213     else mk_apps t vars\r
 214   (* in let rec already_applied = function\r
 215     | Tapp(_, t) -> t = zero || t = dummy || hd t = zero\r
 216     | _ -> false *)\r
 217   in if ends_with t dummy then (app_map, forbidden, t) else (match t with\r
 218   | Tapp(t1, t2, b) ->\r
 219     if b\r
 220     then\r
 221       let app_map, forbidden, t1 = last_round k (app_map, forbidden, t1)\r
 222       in let app_map, forbidden, t2 = last_round k (app_map, forbidden, t2)\r
 223       in app_map, forbidden, Tapp(t1, t2, b)\r
 224     else\r
 225       let app_map, forbidden, t1 = last_round k (app_map, forbidden, t1)\r
 226       in let app_map, forbidden, t2 =\r
 227         try\r
 228             let vars = List.assoc t1 app_map\r
 229             in last_round k (app_map, forbidden, (mk_apps' forbidden t2 vars))\r
 230           with Not_found ->\r
 231             let vars = mk_vars k in\r
 232             let app_map = (t1, vars) :: app_map in\r
 233             last_round k (app_map, (vars @ forbidden), (mk_apps' forbidden t2 vars))\r
 234       in app_map, forbidden, Tapp(t1, t2, true)\r
 235   | _ as t -> app_map, forbidden, t\r
 236   )\r
 237 ;;\r
 238 \r
 239 let fixpoint f =\r
 240   let rec aux x = try\r
 241     let y = f x in aux y\r
 242   with Not_found -> x\r
 243   in aux\r
 244 ;;\r
 245 \r
 246 (* lista di sottotermini applicativi *)\r
 247 let rec subterms = function\r
 248   | Tlam _ -> assert false\r
 249   | Tvar _ as v -> [v]\r
 250   | Tapp(t1, t2, b) -> Tapp(t1, t2, b) :: ((subterms t1) @ (subterms t2))\r
 251 ;;\r
 252 \r
 253 (* filtra dai sottotermini le variabili *)\r
 254 let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;\r
 255 \r
 256 let stupid_sort_uniq map l =\r
 257   let rec stupid_uniq = function\r
 258     | [] -> []\r
 259     | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)\r
 260   in let stupid_compare a b =\r
 261     let rec size = function\r
 262       | Tvar n as v -> if v = zero then 0 else (\r
 263         try\r
 264           let t, _ = List.find (fun (_,vars) -> List.mem v vars) map\r
 265           in 1 + size t\r
 266         with Not_found -> 1 + n)\r
 267       | Tapp(t1,t2,_) -> 1 + size t1 + size t2\r
 268       | Tlam _ -> assert false\r
 269     in compare (size a) (size b)\r
 270   in stupid_uniq (List.sort stupid_compare l)\r
 271 ;;\r
 272 \r
 273 (* crea i match ricorsivamente.\r
 274   - k e' lo special-K\r
 275   - subs e' l'insieme dei sottotermini\r
 276   TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione\r
 277  *)\r
 278 let crea_match subs map forbidden (acc : (term * Num.nf) list) : term -> Num.nf =\r
 279   let req t = try List.assoc t acc with Not_found -> `Var 9999 in\r
 280   let aux t1 = (\r
 281   if t1 = dummy then `Var 99999 else\r
 282   (* let _ = print_term t1 in *)\r
 283   let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2,true)) subs) subs\r
 284   in if cont = [] then\r
 285     try `N (Util.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else\r
 286 \r
 287     if List.mem (hd t1) forbidden then `Lam (true,req (Tapp(t1, dummy, true)))\r
 288     else (\r
 289       let vars = List.assoc t1 map\r
 290       (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))\r
 291       in let _ = print_term (mk_apps dummy vars) *)\r
 292       in let vars = List.map req vars\r
 293       in let vars = List.map (Num.lift 1) vars (* forse lift non necessario *)\r
 294       in let vars = Listx.from_list vars\r
 295       in let body = `I(0, vars)\r
 296       in let branches = List.map (fun t2 -> (Util.index_of t2 subs, req (Tapp(t1, t2, true)))) cont\r
 297       in let bs = ref(branches)\r
 298       in let lift = 1\r
 299       in let args = []\r
 300       in `Lam (true, `Match(body, lift, bs, args))\r
 301     )\r
 302   ) in aux\r
 303 ;;\r
 304 \r
 305 (* filtra dai sottotermini le variabili *)\r
 306 let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;\r
 307 \r
 308 let mk_zeros k =\r
 309   let rec aux n prev =\r
 310     if n = 0 then [zero]\r
 311     else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev\r
 312   in aux (k+1) []\r
 313 ;;\r
 314 \r
 315 let rec freevars = function\r
 316   | Tvar _ as v -> [v]\r
 317   | Tlam(v,t) -> List.filter (fun x-> x <> Tvar v) (freevars t)\r
 318   | Tapp(t1,t2,_) -> (freevars t1) @ (freevars t2)\r
 319 ;;\r
 320 \r
 321 open Pure;;\r
 322 \r
 323 let is_scott_n t n =\r
 324   let open Lambda4 in let open Pure in\r
 325   let rec aux n = function\r
 326   | L (L (A (V 1, L (V 0)))) -> n = 0\r
 327   | L (L (A (V 0, t))) -> aux (n-1) t\r
 328   | _ -> assert false\r
 329   in aux n t\r
 330 ;;\r
 331 let is_scott =\r
 332   let open Lambda4 in let open Pure in\r
 333   let rec aux = function\r
 334   | L (L (A (V 1, L (V 0)))) -> 0\r
 335   | L (L (A (V 0, t))) -> 1 + aux t\r
 336   | _ -> assert false\r
 337   in aux\r
 338 ;;\r
 339 \r
 340 let compute_special_k tms =\r
 341   let rec aux k t = match t with\r
 342     | Tvar _ -> 0\r
 343     | Tapp(t1,t2,_) -> Pervasives.max (aux 0 t1) (aux 0 t2)\r
 344     | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)\r
 345   in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms\r
 346 ;;\r
 347 \r
 348 let magic strings =\r
 349   let rec map_helper_3 a b f =\r
 350     function\r
 351     | [] -> a, b, []\r
 352     | c::cs ->\r
 353       let a, b, d = f (a, b, c) in\r
 354       let a, b, ds = map_helper_3 a b f cs in\r
 355       a, b, (d::ds)\r
 356   in let _ = print_hline ()\r
 357   in let tms = parse strings\r
 358   in let k = compute_special_k tms\r
 359   in let zero' = make_lambda_zero (k+1)\r
 360   in let tms = List.map (fun x -> Tapp(x, zero', false)) tms\r
 361   in let fv = Util.sort_uniq (List.concat (List.map freevars tms))\r
 362   in let (map, tms') = fixpoint (round k) ([], tms)\r
 363   (* in let _ = print_string_endline "map1 "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok1" *)\r
 364   in let _ = List.map print_term tms'\r
 365 \r
 366   in let map1 = List.map fst map\r
 367   in let map2 = List.map snd map\r
 368   in let map_new, forbidden, map1' = map_helper_3 [] [zero] (last_round k) map1\r
 369 \r
 370   in let map = map_new @ (List.combine map1' map2)\r
 371   (* in let _ = print_string_endline "map2 "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok2" *)\r
 372   in let map, forbidden, tms' = map_helper_3 map forbidden (last_round k) tms'\r
 373 \r
 374   in let _ = List.map print_term tms'\r
 375   in let subs = List.concat (List.map subterms tms')\r
 376   in let subs = stupid_sort_uniq map subs\r
 377   (* metti gli zeri in testa, perche' vanno calcolati per primi *)\r
 378   in let zeros = mk_zeros k\r
 379   in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)\r
 380 \r
 381   (* in let _ = print_string_endline " subs"; List.iter print_term subs *)\r
 382   (* in let _ = print_string_endline "map "; List.iter (fun (t,_) -> print_term t) map; print_string_endline "ok" *)\r
 383 \r
 384   in let f t acc = let res = crea_match subs map forbidden acc t in (t,res)::acc\r
 385   in let acc = List.fold_right f subs []\r
 386 \r
 387   in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc\r
 388   in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " &#8614; ") ^^ fancy_of_nf y)) sigma\r
 389 \r
 390   in let _ = print_string_endline "controllo di purezza";\r
 391   (* in let open Num *)\r
 392   in let ps, _ = Num.parse' strings\r
 393   in let ps = List.map (fun x -> Num.mk_app x (`Var 1010)) ps\r
 394   in let ps = List.map (fun t -> Num.ToScott.t_of_nf (t :> Num.nf)) ps\r
 395   in let sigma = List.map (\r
 396     function (Tvar n , inst) -> n, Num.ToScott.t_of_nf inst | _ -> assert false\r
 397     ) sigma\r
 398   (* in let ps =\r
 399     List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma\r
 400   in let _ = List.iteri (fun i n ->\r
 401     print_string_endline ("X " ^ Pure.print (Pure.whd n));\r
 402     (* assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs)) *)\r
 403     is_scott (Pure.whd n); ()\r
 404     ) ps *)\r
 405   in ()\r
 406 ;;\r
 407 \r
 408 \r
 409 (* magic ["x (x x x)"; "x (y. y x)"; "x x (y. y y (x x y))"] ;; *)\r
 410 magic ["((x x) (x. x))";"x x"];;\r
 411 \r
 412 (*\r
 413 \r
 414 let alive (_, _, n) = n;;\r
 415 let rec setalive c = function\r
 416   | Tvar(a,b,_) as v -> if v <> zero && v <> dummy then Tvar(a,b,c) else v\r
 417   | Tapp(a,b) -> Tapp(setalive c a, setalive c b)\r
 418   | Tlam(n, t) -> Tlam(n, setalive c t)\r
 419 ;;\r
 420 \r
 421 let mk_vars t lev =\r
 422   let rec aux n =\r
 423     if n = 0\r
 424     then []\r
 425     else Tvar(0, Some(n, t), lev) :: (aux (n-1))\r
 426   in aux\r
 427 ;;\r
 428 \r
 429 let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)\r
 430 \r
 431 \r
 432 let compute_special_k tms =\r
 433   let rec aux k t = match t with\r
 434     | Tvar _ -> 0\r
 435     | Tapp(t1,t2) -> Pervasives.max (aux 0 t1) (aux 0 t2)\r
 436     | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)\r
 437   in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms\r
 438 ;;\r
 439 \r
 440 let compute_special_h tms =\r
 441   let rec eat_lam = function\r
 442     | Tlam(_,t) -> eat_lam t\r
 443     | _ as t -> t\r
 444   in\r
 445   let rec aux t = match t with\r
 446     | Tvar _ -> 0\r
 447     | Tapp(t1,t2) -> Pervasives.max (aux t1) (aux t2)\r
 448     | Tlam(v,t) -> 1 + (aux (eat_lam t))\r
 449   in 1 + List.fold_left (fun b a -> Pervasives.max (aux a) b) 0 tms\r
 450 ;;\r
 451 \r
 452 (* funzione di traduzione brutta & cattiva *)\r
 453 let translate k =\r
 454   let rec aux = function\r
 455   | Tlam _ -> assert false\r
 456   | Tvar _ as v -> v\r
 457   | Tapp(t1, t2) ->\r
 458     let v = hd t1 in\r
 459     let a = alive v in\r
 460     let t1' = aux t1 in\r
 461     let t2' = if a = 0\r
 462       then t2\r
 463       else mk_apps t2 ((List.rev (mk_vars t1' (a-1) k)) @ [zero])\r
 464     in Tapp(t1', aux t2')\r
 465   in aux\r
 466 ;;\r
 467 \r
 468 (* sostituisce gli argomenti dummy (delle variabili morte) con 'dummy' *)\r
 469 let rec dummize = function\r
 470   | Tlam _ -> assert false\r
 471   | Tvar (a,Some(b,t), c) -> Tvar(a, Some (b, dummize t), c)\r
 472   | Tvar _ as v -> v\r
 473   | Tapp(t1, t2) ->\r
 474     if alive (hd t1) = 0\r
 475     then Tapp(dummize t1, dummy)\r
 476     else Tapp(dummize t1, dummize t2)\r
 477 ;;\r
 478 \r
 479 (* lista di sottotermini applicativi *)\r
 480 let rec subterms = function\r
 481   | Tlam _ -> assert false\r
 482   | Tvar _ as v -> [v]\r
 483   | Tapp(t1, t2) -> Tapp(t1, t2) :: ((subterms t1) @ (subterms t2))\r
 484 ;;\r
 485 \r
 486 (* filtra dai sottotermini le variabili *)\r
 487 let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;\r
 488 \r
 489 \r
 490 let rec stupid_uniq = function\r
 491   | [] -> []\r
 492   | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)\r
 493 ;;\r
 494 let stupid_compare a b =\r
 495   let rec size = function\r
 496     | Tvar(_,None,_) -> 0\r
 497     | Tvar(_,Some(_,t),_) -> 1 + size t\r
 498     | Tapp(t1,t2) -> 1 + size t1 + size t2\r
 499     | Tlam _ -> assert false\r
 500   in compare (size a) (size b)\r
 501 ;;\r
 502 let stupid_sort_uniq l = stupid_uniq (List.sort stupid_compare l);;\r
 503 \r
 504 (* crea i match ricorsivamente.\r
 505   - k e' lo special-K\r
 506   - subs e' l'insieme dei sottotermini\r
 507   TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione\r
 508  *)\r
 509 let crea_match k subs (acc : (term * Lambda3.nf) list) : term -> Lambda3.nf =\r
 510   let req t = try List.assoc t acc with Not_found -> `Var 9999 in\r
 511   let aux t1 = (\r
 512   if t1 = dummy then `Var 99999 else\r
 513   (* let _ = print_term t1 in *)\r
 514   let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2)) subs) subs\r
 515   in if cont = [] then\r
 516     try `N (Lambda3.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else\r
 517   let a = alive (hd t1) in\r
 518     if a = 0 then `Lam (req (Tapp(t1, dummy)))\r
 519     else (\r
 520       let vars = (List.rev (mk_vars t1 (a-1) k)) @ [zero]\r
 521       (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))\r
 522       in let _ = print_term (mk_apps dummy vars) *)\r
 523       in let vars = List.map req vars\r
 524       in let vars = List.map (Lambda3.lift 1) vars (* forse lift non necessario *)\r
 525       in let vars = Listx.from_list vars\r
 526       in let body = `I(0, vars)\r
 527       in let branches = List.map (fun t2 -> (Lambda3.index_of t2 subs, req (Tapp(t1, t2)))) cont\r
 528       in let bs = ref(branches)\r
 529       in let lift = 1\r
 530       in let args = []\r
 531       in `Lam (`Match(body, lift, bs, args))\r
 532     )\r
 533   ) in aux\r
 534 ;;\r
 535 \r
 536 let mk_zeros k =\r
 537   let rec aux n prev =\r
 538     if n = 0 then [zero]\r
 539     else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev\r
 540   in aux (k+1) []\r
 541 ;;\r
 542 \r
 543 let is_scott_n t n =\r
 544   let open Lambda3 in let open Pure in\r
 545   let rec aux n = function\r
 546   | L (L (A (V 1, L (V 0)))) -> n = 0\r
 547   | L (L (A (V 0, t))) -> aux (n-1) t\r
 548   | _ -> assert false\r
 549   in aux n t\r
 550 ;;\r
 551 \r
 552 (* do the magic *)\r
 553 let magic strings k h = (\r
 554   let tms = parse strings\r
 555   in let tms = List.map (fun x -> Tapp(x, zero)) tms\r
 556   in let tms' = List.map (setalive h) tms\r
 557   in let tms' = List.map (translate k) tms'\r
 558   in let tms' = List.map dummize tms'\r
 559   (* in let bullet = ">" / "&bullet;" *)\r
 560   (* in let progress s = print_endline (bullet ^^ fancy_of_string s) *)\r
 561   in let progress = print_h1\r
 562   in let _ = progress "traduzione completata"\r
 563   (* in let _ = List.map print_term tms' *)\r
 564   in let _ = progress "ordino i sottotermini"\r
 565   in let subs = List.concat (List.map subterms tms')\r
 566   in let subs = stupid_sort_uniq subs\r
 567   (* metti gli zeri in testa, perche' vanno calcolati per primi *)\r
 568   in let zeros = mk_zeros k\r
 569   in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)\r
 570   in let _ = progress ("sottotermini generati: " ^ string_of_int (List.length subs))\r
 571   in let vars = vars subs\r
 572   (* in let _ = List.iter print_term subs *)\r
 573   (* in let _ = 0/0 *)\r
 574   in let fv = List.filter (function Tvar(_, None, _) as v -> v <> dummy | _ -> false) vars\r
 575   (* in let _ = print_string ("> free vars: " ^ String.concat ", " (List.map (string_of_term) fv)) *)\r
 576   in let _ = progress "sto creando i match"\r
 577   (* in let sigma = List.map (fun x -> x, crea_match k subs x) fv *)\r
 578   in let f t acc = let res = crea_match k subs acc t in (t,res)::acc\r
 579   in let acc = List.fold_right f subs []\r
 580   in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc\r
 581   in let _ = progress "match creati"\r
 582   in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " &#8614; ") ^^ fancy_of_nf y)) sigma\r
 583 \r
 584   in let _ = progress "controllo di purezza";\r
 585   in let open Lambda3\r
 586   in let ps, _ = Lambda3.parse' strings\r
 587   in let ps = List.map (fun x -> Lambda3.mk_app x (`Var 1010)) ps\r
 588   in let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) ps\r
 589   in let sigma = List.map (\r
 590     function (Tvar(n,_,_), inst) -> n, ToScott.t_of_nf inst | _ -> assert false\r
 591     ) sigma\r
 592   in let ps =\r
 593     List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma\r
 594   in let _ = List.iteri (fun i n ->\r
 595     (* print_string_endline ((string_of_int i) ^ ":: " ^ (Pure.print (Pure.whd n))); *)\r
 596     (* assert (Pure.whd n = Scott.mk_n (Lambda3.index_of (List.nth tms' i) subs))) ps *)\r
 597     assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs))) ps\r
 598   in let _ = progress "fatto." in ()\r
 599 );;\r
 600 \r
 601 let do_everything tms =\r
 602 let tms' = parse tms in\r
 603 let k = compute_special_k tms' in\r
 604 let h = compute_special_h tms' in\r
 605 (* let _ = print_string_endline (string_of_int h) in *)\r
 606 magic tms k h\r
 607 ;;\r
 608 \r
 609 let _ =\r
 610   let tms = ["a a"; "a b"; "b a"; "b (x. y.x y a)"] in\r
 611   (* 1 2 *)\r
 612   (* let tms = ["x c" ; "b (x c d e)"; "b"] in *)\r
 613   (* 0 1 *)\r
 614   (* let tms = ["x x x"] in *)\r
 615   let tms' = parse tms in\r
 616   let k = compute_special_k tms' in\r
 617   let h = compute_special_h tms' in\r
 618   (* let _ = print_string_endline (string_of_int h) in *)\r
 619   magic tms k h\r
 620 ;;\r
 621 \r
 622 (* type var' = (* unique name *) int * (int * term') option * (*dead*) bool option\r
 623 and term' =\r
 624   | Tvar' of var'\r
 625   | Tapp' of term' * term' * (* active *) bool\r
 626   | Tlam' of int * term'\r
 627 ;;\r
 628 \r
 629 let rec iter mustapply =\r
 630   let aux = function\r
 631   | Tvar'(n, Some(m,t), b) -> Tvar(n, Some(m, aux t), b)\r
 632   | Tvar' _ as v -> v\r
 633   | Tapp'(t1, t2, b) -> if b &&\r
 634   in aux\r
 635 ;; *)\r
 636 \r
 637 *)\r