ocaml/andrea3.ml

   1 type var = (* unique name *) int * (int * term) option * (*level*) int\r
   2 and term =\r
   3   | Tvar of var\r
   4   | Tapp of term * term\r
   5   | Tlam of int * term\r
   6 ;;\r
   7 \r
   8 let zero = Tvar(1010, None, 0);;\r
   9 let dummy = Tvar(333, None, 0);;\r
  10 \r
  11 (* mk_app & subst implementano la beta *)\r
  12 let rec mk_app t1 t2 = match t1 with\r
  13   | Tlam(v, t1') -> subst v t2 t1'\r
  14   | _ -> Tapp(t1, t2)\r
  15 and subst v tv =\r
  16   let rec aux = function\r
  17   | Tapp(t1, t2) -> mk_app (aux t1) (aux t2)\r
  18   | Tvar(v', _, _) as t -> if v = v' then tv else t\r
  19   | Tlam(v', t') as t -> if v = v' then t else Tlam(v', aux t')\r
  20   in aux\r
  21 ;;\r
  22 \r
  23 (* PARSING AND PRINTING *)\r
  24 \r
  25 let parse =\r
  26   let rec minus1 = function\r
  27     | Tvar(n, None, x) -> Tvar(n-1, None, x)\r
  28     | Tvar _ -> assert false\r
  29     | Tapp(t1, t2) -> Tapp(minus1 t1, minus1 t2)\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, None, 0)\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 List.nth free (n) else List.nth bound (-n-1) 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, None, _) -> (string_of_int' n)\r
  54     (* | (_, Some(n,t), _) -> "?" ^ string_of_int n *)\r
  55     | (_, Some(n,t), _) -> "{" ^ (string_of_term_no_pars t) ^ "|" ^ (string_of_int n) ^ "}"\r
  56   and string_of_term_w_pars = function\r
  57     | Tvar v -> string_of_var v\r
  58     | Tapp(t1, t2) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"\r
  59     | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"\r
  60   and string_of_term_no_pars_app = function\r
  61     | Tapp(t1, t2) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)\r
  62     | _ as t -> string_of_term_w_pars t\r
  63   and string_of_term_no_pars_lam = function\r
  64     | Tlam(v, t) -> "λ" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)\r
  65     | _ as t -> string_of_term_no_pars t\r
  66   and string_of_term_no_pars = function\r
  67     | Tlam(_, _) as t -> string_of_term_no_pars_lam t\r
  68     | _ as t -> string_of_term_no_pars_app t\r
  69   in string_of_term_no_pars\r
  70 in let rec html_of_term =\r
  71   let free = ["a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"] in\r
  72   let bound = ["x"; "y"; "z"; "w"; "q"] in\r
  73   let string_of_int' n = if n >= 0 then List.nth free (n) else List.nth bound (-n-1) in\r
  74   let rec string_of_var t =\r
  75     if Tvar t = dummy then "&num;" else if Tvar t = zero then "Z" else match t with\r
  76     | (n, None, _) -> (string_of_int' n)\r
  77     | (_, Some(n,t), _) -> "&alpha;<sup>" ^ (string_of_term_no_pars t) ^ "</sup><sub>" ^ (string_of_int n) ^ "</sub>"\r
  78   and string_of_term_w_pars = function\r
  79     | Tvar v -> string_of_var v\r
  80     | Tapp(t1, t2) -> "(" ^ (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2) ^ ")"\r
  81     | Tlam(_,_) as t -> "(" ^ (string_of_term_no_pars_lam t) ^ ")"\r
  82   and string_of_term_no_pars_app = function\r
  83     | Tapp(t1, t2) -> (string_of_term_no_pars_app t1) ^ " " ^ (string_of_term_w_pars t2)\r
  84     | _ as t -> string_of_term_w_pars t\r
  85   and string_of_term_no_pars_lam = function\r
  86     | Tlam(v, t) -> "&lambda;" ^ (string_of_int' v) ^ ". " ^ (string_of_term_no_pars_lam t)\r
  87     | _ as t -> string_of_term_no_pars t\r
  88   and string_of_term_no_pars = function\r
  89     | Tlam(_, _) as t -> string_of_term_no_pars_lam t\r
  90     | _ as t -> string_of_term_no_pars_app t\r
  91   in string_of_term_no_pars\r
  92 in\r
  93   string_of_term t / html_of_term t\r
  94 ;;\r
  95 \r
  96 let fancy_of_nf t: Console.fancyobj =\r
  97 let rec print ?(l=[]) =\r
  98  function\r
  99     `Var n -> Lambda3.print_name l n\r
 100   | `N n -> string_of_int n\r
 101   | `Match(t,bs_lift,bs,args) ->\r
 102      "([" ^ print ~l (t :> Lambda3.nf) ^\r
 103      " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (Lambda3.lift bs_lift t)) !bs) ^ "] " ^\r
 104      String.concat " " (List.map (print ~l) args) ^ ")"\r
 105   | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"\r
 106   | `Lam nf ->\r
 107      let name = Lambda3.string_of_var (List.length l) in\r
 108      "" ^ name ^ "." ^ print ~l:(name::l) (nf : Lambda3.nf)\r
 109 \r
 110 in let rec print_html ?(l=[]) =\r
 111  function\r
 112     `Var n -> Lambda3.print_name l n\r
 113   | `N n -> string_of_int n\r
 114   | `Match(t,bs_lift,bs,args) ->\r
 115      "(<b>match</b> " ^ print_html ~l (t :> Lambda3.nf) ^\r
 116      " <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
 117   | `I(n,args) -> "(" ^ Lambda3.print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print_html ~l) args)) ^ ")"\r
 118   | `Lam nf ->\r
 119      let name = Lambda3.string_of_var (List.length l) in\r
 120      "&lambda;" ^ name ^ ". " ^ print_html ~l:(name::l) (nf : Lambda3.nf)\r
 121 in\r
 122   print t / print_html t\r
 123 ;;\r
 124 \r
 125 let print_term t = print_endline (fancy_of_term t :> Console.fancyobj);;\r
 126 (*  *)\r
 127 \r
 128 \r
 129 let varcount = ref 0;;\r
 130 \r
 131 let freshvar () = (\r
 132   varcount := (!varcount + 1);\r
 133   !varcount\r
 134 );;\r
 135 \r
 136 let rec hd =\r
 137   function\r
 138   | Tvar x -> x\r
 139   | Tapp(t1,t2) -> hd t1\r
 140   | Tlam _ -> assert false\r
 141 ;;\r
 142 \r
 143 let alive (_, _, n) = n;;\r
 144 let rec setalive c = function\r
 145   | Tvar(a,b,_) as v -> if v <> zero && v <> dummy then Tvar(a,b,c) else v\r
 146   | Tapp(a,b) -> Tapp(setalive c a, setalive c b)\r
 147   | Tlam(n, t) -> Tlam(n, setalive c t)\r
 148 ;;\r
 149 \r
 150 let mk_vars t lev =\r
 151   let rec aux n =\r
 152     if n = 0\r
 153     then []\r
 154     else Tvar(0, Some(n, t), lev) :: (aux (n-1))\r
 155   in aux\r
 156 ;;\r
 157 \r
 158 let mk_apps t ts = List.fold_right (fun x y -> mk_app y x) (List.rev ts) t;; (* which FOLD? FIXME *)\r
 159 \r
 160 \r
 161 let compute_special_k tms =\r
 162   let rec aux k t = match t with\r
 163     | Tvar _ -> 0\r
 164     | Tapp(t1,t2) -> Pervasives.max (aux 0 t1) (aux 0 t2)\r
 165     | Tlam(v,t) -> Pervasives.max (k+1) (aux (k + 1) t)\r
 166   in List.fold_left (fun b a -> Pervasives.max (aux 0 a) b) 0 tms\r
 167 ;;\r
 168 \r
 169 let compute_special_h tms =\r
 170   let rec eat_lam = function\r
 171     | Tlam(_,t) -> eat_lam t\r
 172     | _ as t -> t\r
 173   in\r
 174   let rec aux t = match t with\r
 175     | Tvar _ -> 0\r
 176     | Tapp(t1,t2) -> Pervasives.max (aux t1) (aux t2)\r
 177     | Tlam(v,t) -> 1 + (aux (eat_lam t))\r
 178   in 1 + List.fold_left (fun b a -> Pervasives.max (aux a) b) 0 tms\r
 179 ;;\r
 180 \r
 181 (* funzione di traduzione brutta & cattiva *)\r
 182 let translate k =\r
 183   let rec aux = function\r
 184   | Tlam _ -> assert false\r
 185   | Tvar _ as v -> v\r
 186   | Tapp(t1, t2) ->\r
 187     let v = hd t1 in\r
 188     let a = alive v in\r
 189     let t1' = aux t1 in\r
 190     let t2' = if a = 0\r
 191       then t2\r
 192       else mk_apps t2 ((List.rev (mk_vars t1' (a-1) k)) @ [zero])\r
 193     in Tapp(t1', aux t2')\r
 194   in aux\r
 195 ;;\r
 196 \r
 197 (* sostituisce gli argomenti dummy (delle variabili morte) con 'dummy' *)\r
 198 let rec dummize = function\r
 199   | Tlam _ -> assert false\r
 200   | Tvar (a,Some(b,t), c) -> Tvar(a, Some (b, dummize t), c)\r
 201   | Tvar _ as v -> v\r
 202   | Tapp(t1, t2) ->\r
 203     if alive (hd t1) = 0\r
 204     then Tapp(dummize t1, dummy)\r
 205     else Tapp(dummize t1, dummize t2)\r
 206 ;;\r
 207 \r
 208 (* lista di sottotermini applicativi *)\r
 209 let rec subterms = function\r
 210   | Tlam _ -> assert false\r
 211   | Tvar _ as v -> [v]\r
 212   | Tapp(t1, t2) -> Tapp(t1, t2) :: ((subterms t1) @ (subterms t2))\r
 213 ;;\r
 214 \r
 215 (* filtra dai sottotermini le variabili *)\r
 216 let rec vars subs = List.filter (function Tvar _ -> true | _ -> false) subs;;\r
 217 \r
 218 \r
 219 let rec stupid_uniq = function\r
 220   | [] -> []\r
 221   | x::xs -> if List.mem x xs then (stupid_uniq xs) else x::(stupid_uniq xs)\r
 222 ;;\r
 223 let stupid_compare a b =\r
 224   let rec size = function\r
 225     | Tvar(_,None,_) -> 0\r
 226     | Tvar(_,Some(_,t),_) -> 1 + size t\r
 227     | Tapp(t1,t2) -> 1 + size t1 + size t2\r
 228     | Tlam _ -> assert false\r
 229   in compare (size a) (size b)\r
 230 ;;\r
 231 let stupid_sort_uniq l = stupid_uniq (List.sort stupid_compare l);;\r
 232 \r
 233 (* crea i match ricorsivamente.\r
 234   - k e' lo special-K\r
 235   - subs e' l'insieme dei sottotermini\r
 236   TODO: riscrivere la funzione per evitare/ottimizzare la ricorsione\r
 237  *)\r
 238 let crea_match k subs (acc : (term * Lambda3.nf) list) : term -> Lambda3.nf =\r
 239   let req t = try List.assoc t acc with Not_found -> `Var 9999 in\r
 240   let aux t1 = (\r
 241   if t1 = dummy then `Var 99999 else\r
 242   (* let _ = print_term t1 in *)\r
 243   let cont = List.filter (fun t2 -> List.mem (Tapp(t1,t2)) subs) subs\r
 244   in if cont = [] then\r
 245     try `N (Lambda3.index_of t1 subs) with Not_found -> `Var 999 (* variabile dummy qui *) else\r
 246   let a = alive (hd t1) in\r
 247     if a = 0 then `Lam (req (Tapp(t1, dummy)))\r
 248     else (\r
 249       let vars = (List.rev (mk_vars t1 (a-1) k)) @ [zero]\r
 250       (* in let _ = print_endline (String.concat " " (List.map string_of_term vars))\r
 251       in let _ = print_term (mk_apps dummy vars) *)\r
 252       in let vars = List.map req vars\r
 253       in let vars = List.map (Lambda3.lift 1) vars (* forse lift non necessario *)\r
 254       in let vars = Listx.from_list vars\r
 255       in let body = `I(0, vars)\r
 256       in let branches = List.map (fun t2 -> (Lambda3.index_of t2 subs, req (Tapp(t1, t2)))) cont\r
 257       in let bs = ref(branches)\r
 258       in let lift = 1\r
 259       in let args = []\r
 260       in `Lam (`Match(body, lift, bs, args))\r
 261     )\r
 262   ) in aux\r
 263 ;;\r
 264 \r
 265 let mk_zeros k =\r
 266   let rec aux n prev =\r
 267     if n = 0 then [zero]\r
 268     else let prev = aux (n-1) prev in let x = mk_app (List.hd prev) dummy in x :: prev\r
 269   in aux (k+1) []\r
 270 ;;\r
 271 \r
 272 let is_scott_n t n =\r
 273   let open Lambda3 in let open Pure in\r
 274   let rec aux n = function\r
 275   | L (L (A (V 1, L (V 0)))) -> n = 0\r
 276   | L (L (A (V 0, t))) -> aux (n-1) t\r
 277   | _ -> assert false\r
 278   in aux n t\r
 279 ;;\r
 280 \r
 281 (* do the magic *)\r
 282 let magic strings k h = (\r
 283   let tms = parse strings\r
 284   in let tms = List.map (fun x -> Tapp(x, zero)) tms\r
 285   in let tms' = List.map (setalive h) tms\r
 286   in let tms' = List.map (translate k) tms'\r
 287   in let tms' = List.map dummize tms'\r
 288   in let progress s = print_bullet (fancy_of_string s)\r
 289   in let _ = progress "traduzione completata"\r
 290   (* in let _ = List.map print_term tms' *)\r
 291   in let _ = progress "ordino i sottotermini"\r
 292   in let subs = List.concat (List.map subterms tms')\r
 293   in let subs = stupid_sort_uniq subs\r
 294   (* metti gli zeri in testa, perche' vanno calcolati per primi *)\r
 295   in let zeros = mk_zeros k\r
 296   in let subs = (List.filter (fun t -> not (List.mem t zeros)) subs) @ (List.rev zeros)\r
 297   in let _ = progress ("sottotermini generati: " ^ string_of_int (List.length subs))\r
 298   in let vars = vars subs\r
 299   (* in let _ = List.iter print_term subs *)\r
 300   (* in let _ = 0/0 *)\r
 301   in let fv = List.filter (function Tvar(_, None, _) as v -> v <> dummy | _ -> false) vars\r
 302   (* in let _ = print_string ("> free vars: " ^ String.concat ", " (List.map (string_of_term) fv)) *)\r
 303   in let _ = progress "sto creando i match"\r
 304   (* in let sigma = List.map (fun x -> x, crea_match k subs x) fv *)\r
 305   in let f t acc = let res = crea_match k subs acc t in (t,res)::acc\r
 306   in let acc = List.fold_right f subs []\r
 307   in let sigma = List.filter (fun (t,res) -> List.mem t fv) acc\r
 308   in let _ = progress "match creati"\r
 309   in let _ = List.iter (fun (x,y) -> print_endline (fancy_of_term x ^^ (" : " / " &#8614; ") ^^ fancy_of_nf y)) sigma\r
 310 \r
 311   in let _ = progress "controllo di purezza";\r
 312   in let open Lambda3\r
 313   in let ps, _ = Lambda3.parse' strings\r
 314   in let ps = List.map (fun x -> Lambda3.mk_app x (`Var 1010)) ps\r
 315   in let ps = List.map (fun t -> ToScott.t_of_nf (t :> nf)) ps\r
 316   in let sigma = List.map (\r
 317     function (Tvar(n,_,_), inst) -> n, ToScott.t_of_nf inst | _ -> assert false\r
 318     ) sigma\r
 319   in let ps =\r
 320     List.fold_left (fun ps (x,inst) -> List.map (Pure.subst false x inst) ps) ps sigma\r
 321   in let _ = List.iteri (fun i n ->\r
 322     (* print_string_endline ((string_of_int i) ^ ":: " ^ (Pure.print (Pure.whd n))); *)\r
 323     (* assert (Pure.whd n = Scott.mk_n (Lambda3.index_of (List.nth tms' i) subs))) ps *)\r
 324     assert (is_scott_n (Pure.whd n) (Lambda3.index_of (List.nth tms' i) subs))) ps\r
 325   in let _ = progress "fatto." in ()\r
 326 );;\r
 327 \r
 328 let do_everything tms =\r
 329 let tms' = parse tms in\r
 330 let _ = List.iter print_term tms' in\r
 331 let k = compute_special_k tms' in\r
 332 let h = compute_special_h tms' in\r
 333 (* let _ = print_string_endline (string_of_int h) in *)\r
 334 magic tms k h\r
 335 ;;\r
 336 \r
 337 let _ =\r
 338   let tms = ["a a"; "a b"; "b a"; "b (x. y.x y a)"] in\r
 339   (* 1 2 *)\r
 340   (* let tms = ["x c" ; "b (x c d e)"; "b"] in *)\r
 341   (* 0 1 *)\r
 342   (* let tms = ["x x x"] in *)\r
 343   let tms' = parse tms in\r
 344   let _ = List.iter print_term tms' in\r
 345   let k = compute_special_k tms' in\r
 346   let h = compute_special_h tms' in\r
 347   (* let _ = print_string_endline (string_of_int h) in *)\r
 348   magic tms k h\r
 349 ;;\r
 350 \r
 351 (* type var' = (* unique name *) int * (int * term') option * (*dead*) bool option\r
 352 and term' =\r
 353   | Tvar' of var'\r
 354   | Tapp' of term' * term' * (* active *) bool\r
 355   | Tlam' of int * term'\r
 356 ;;\r
 357 \r
 358 let rec iter mustapply =\r
 359   let aux = function\r
 360   | Tvar'(n, Some(m,t), b) -> Tvar(n, Some(m, aux t), b)\r
 361   | Tvar' _ as v -> v\r
 362   | Tapp'(t1, t2, b) -> if b &&\r
 363   in aux\r
 364 ;; *)\r