ocaml/simple.ml

   1 let (++) f g x = f (g x);;\r
   2 let id x = x;;\r
   3 let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;\r
   4 \r
   5 let print_hline = Console.print_hline;;\r
   6 \r
   7 open Pure\r
   8 \r
   9 type var_flag = bool ;;\r
  10 \r
  11 type var = int;;\r
  12 type t =\r
  13  | V of var\r
  14  | A of var_flag * t * t\r
  15  | L of t\r
  16 ;;\r
  17 \r
  18 let string_of_t =\r
  19   let sep_of_app b = if b then " +" else " " in\r
  20   let string_of_bvar =\r
  21    let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
  22    let bvarsno = List.length bound_vars in\r
  23    fun nn -> if nn < bvarsno then List.nth bound_vars nn else "v" ^ (string_of_int (nn - bvarsno + 1)) in\r
  24   let rec string_of_term_w_pars level = function\r
  25     | V v -> if v >= level then string_of_int (v-level) else\r
  26        string_of_bvar (level - v-1)\r
  27     | A _\r
  28     | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
  29   and string_of_term_no_pars_app level = function\r
  30     | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ sep_of_app b ^ string_of_term_w_pars level t2\r
  31     | _ as t -> string_of_term_w_pars level t\r
  32   and string_of_term_no_pars level = function\r
  33     | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r
  34     | _ as t -> string_of_term_no_pars_app level t\r
  35   in string_of_term_no_pars 0\r
  36 ;;\r
  37 \r
  38 (* does NOT lift the argument *)\r
  39 let mk_lams = fold_nat (fun x _ -> L x) ;;\r
  40 \r
  41 let measure_of_t =\r
  42  let rec aux = function\r
  43  | V _ -> 0\r
  44  | A(b,t1,t2) ->\r
  45    (if b then 1 else 0) + aux t1 + aux t2\r
  46  | L t -> aux t\r
  47  in aux\r
  48 ;;\r
  49 \r
  50 type problem = {\r
  51    orig_freshno: int\r
  52  ; freshno : int\r
  53  ; tms : t list\r
  54  ; sigma : (var * t) list (* substitutions *)\r
  55 }\r
  56 \r
  57 let string_of_problem p =\r
  58  let measure = List.fold_left (+) 0 (List.map measure_of_t p.tms) in\r
  59  let lines = ("[measure] " ^ string_of_int measure) ::\r
  60    List.map (fun x -> "[TM] " ^ string_of_t x) p.tms in\r
  61  String.concat "\n" lines\r
  62 ;;\r
  63 \r
  64 exception Done of (var * t) list (* substitution *);;\r
  65 exception Fail of int * string;;\r
  66 \r
  67 let problem_fail p reason =\r
  68  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
  69  print_endline (string_of_problem p);\r
  70  raise (Fail (-1, reason))\r
  71 ;;\r
  72 \r
  73 let freshvar ({freshno} as p) =\r
  74  {p with freshno=freshno+1}, freshno+1\r
  75 ;;\r
  76 \r
  77 let rec is_inert =\r
  78  function\r
  79  | A(_,t,_) -> is_inert t\r
  80  | V _ -> true\r
  81  | L _ -> false\r
  82 ;;\r
  83 \r
  84 let is_var = function V _ -> true | _ -> false;;\r
  85 let is_lambda = function L _ -> true | _ -> false;;\r
  86 \r
  87 let rec get_inert = function\r
  88  | V n -> (n,0)\r
  89  | A(_,t,_) -> let hd,args = get_inert t in hd,args+1\r
  90  | _ -> assert false\r
  91 ;;\r
  92 \r
  93 (* precomputes the number of leading lambdas in a term,\r
  94    after replacing _v_ w/ a term starting with n lambdas *)\r
  95 let rec no_leading_lambdas v n = function\r
  96  | L t -> 1 + no_leading_lambdas (v+1) n t\r
  97  | A _ as t -> let v', m = get_inert t in if v = v' then max 0 (n - m) else 0\r
  98  | V v' -> if v = v' then n else 0\r
  99 ;;\r
 100 \r
 101 let rec erase = function\r
 102  | L t -> L (erase t)\r
 103  | A(_,t1,t2) -> A(false, erase t1, erase t2)\r
 104  | V _ as t -> t\r
 105 ;;\r
 106 \r
 107 let explode =\r
 108  let rec aux args = function\r
 109  | L _ -> assert false\r
 110  | V _ as x -> x, args\r
 111  | A(b,t1,t2) -> aux ((b,t2)::args) t1\r
 112  in aux []\r
 113 ;;\r
 114 \r
 115 let rec implode hd args =\r
 116  match args with\r
 117  | [] -> hd\r
 118  | (f,a)::args -> implode (A(f,hd,a)) args\r
 119 ;;\r
 120 \r
 121 let get_head =\r
 122  let rec aux lev = function\r
 123  | L t -> aux (lev+1) t\r
 124  | A(_,t,_) -> aux lev t\r
 125  | V v -> v - lev\r
 126  in aux 0\r
 127 ;;\r
 128 \r
 129 let rec subst level delift ((var, tm) as sub) =\r
 130  function\r
 131  | V v -> if v = level + var then lift level tm else V (if delift && v > level then v-1 else v)\r
 132  | L t -> L (subst (level + 1) delift sub t)\r
 133  | A(b,t1,t2) ->\r
 134     let t1' = subst level delift sub t1 in\r
 135     let t2' = subst level delift sub t2 in\r
 136     mk_app b t1' t2'\r
 137 and mk_app flag t1 t2 = match t1 with\r
 138  | L t1 -> subst 0 true (0, t2) t1\r
 139  | _ -> A (flag, t1, t2)\r
 140 and lift n =\r
 141  let rec aux lev =\r
 142   function\r
 143   | V m -> V (if m >= lev then m + n else m)\r
 144   | L t -> L(aux (lev+1) t)\r
 145   | A (b,t1, t2) -> A (b,aux lev t1, aux lev t2)\r
 146  in aux 0\r
 147 ;;\r
 148 let subst = subst 0 false;;\r
 149 (* let mk_app = mk_app true;; *)\r
 150 let rec mk_apps t = function\r
 151  | [] -> t\r
 152  | (f,x)::xs -> mk_apps (mk_app f t x) xs\r
 153 ;;\r
 154 \r
 155 let eta_eq =\r
 156  let rec aux t1 t2 = match t1, t2 with\r
 157   | L t1, L t2 -> aux t1 t2\r
 158   | L t1, t2 -> aux t1 (A(false,lift 1 t2,V 0))\r
 159   | t1, L t2 -> aux (A(false,lift 1 t1,V 0)) t2\r
 160   | V a, V b -> a = b\r
 161   | A(_,t1,t2), A(_,u1,u2) -> aux t1 u1 && aux t2 u2\r
 162   | _, _ -> false\r
 163  in aux ;;\r
 164 \r
 165 (* is arg1 eta-subterm of arg2 ? *)\r
 166 let eta_subterm u =\r
 167  let rec aux lev t = eta_eq u (lift lev t) || match t with\r
 168  | L t -> aux (lev+1) t\r
 169  | A(_, t1, t2) -> aux lev t1 || aux lev t2\r
 170  | _ -> false\r
 171  in aux 0\r
 172 ;;\r
 173 \r
 174 let subst_in_problem ?(top=true) ((v, t) as sub) p =\r
 175 print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);\r
 176  let sigma = sub::p.sigma in\r
 177  let sub = (v, t) in\r
 178  let tms = List.map (subst sub) p.tms in\r
 179  {p with tms; sigma}\r
 180 ;;\r
 181 \r
 182 let rec purify = function\r
 183  | L t -> Pure.L (purify t)\r
 184  | A(_,t1,t2) -> Pure.A (purify t1, purify t2)\r
 185  | V n -> Pure.V n\r
 186 ;;\r
 187 \r
 188 let check p sigma =\r
 189  assert false (* FIXME *)\r
 190  (* print_endline "Checking...";\r
 191  let tms = List.map purify p.tms in\r
 192  let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r
 193  let freshno = List.fold_right (max ++ fst) sigma 0 in\r
 194  let env = Pure.env_of_sigma freshno sigma in\r
 195  assert (Pure.diverged (Pure.mwhd (env,div,[])));\r
 196  print_endline " D diverged.";\r
 197  assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));\r
 198  print_endline " C converged.";\r
 199  () *)\r
 200 ;;\r
 201 \r
 202 let sanity p =\r
 203  print_endline (string_of_problem p); (* non cancellare *)\r
 204  let rec all_different = function\r
 205   | [] -> true\r
 206   | x::xs -> List.for_all ((<>) x) xs && all_different xs in\r
 207  if List.for_all is_var p.tms && all_different p.tms\r
 208   then raise (Done p.sigma);\r
 209  if List.exists (not ++ is_inert) p.tms\r
 210   then problem_fail p "used a non-effective path";\r
 211  p\r
 212 ;;\r
 213 \r
 214 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 215 \r
 216 let step var j n p =\r
 217   let atsnd f (a,b) = (a, f b) in\r
 218   let p, alphas = (* make fresh vars *)\r
 219    fold_nat (fun (p, vs) _ ->\r
 220      let p, v = freshvar p in\r
 221      p, v::vs\r
 222    ) (p, []) n in let alphas = List.rev alphas in\r
 223   let rec aux lev (inside:bool) = function\r
 224   | L t -> L (aux (lev+1) inside t)\r
 225   | _ as x ->\r
 226     let hd, args = explode x in\r
 227     if hd = V (var+lev) then\r
 228       (let nargs = List.length args in\r
 229        let k = max 0 (j + 1 - nargs) in\r
 230        let args = List.mapi\r
 231         (fun i (f, t) -> f, lift k (aux lev (if i=j then true else inside) t)) args in\r
 232        let bound = fold_nat (fun x n -> (false,V(n-1)) :: x) [] k in\r
 233        let args = args @ bound in\r
 234        let _, head = List.nth args j in\r
 235        let args = List.mapi\r
 236         (fun i (f, t) -> (if i=j && not inside then false else f), if i=j && not inside then erase t else t) args in\r
 237        let head = (if inside then erase else id) head in\r
 238        print_endline ("HEAD: " ^ string_of_t head);\r
 239        let alphas = List.map (fun v -> false, V(lev+k+v)) alphas in\r
 240        let t = mk_apps head (alphas @ args) in\r
 241        let t = mk_lams t k in\r
 242        t\r
 243     ) else\r
 244     (let args = List.map (atsnd (aux lev inside)) args in\r
 245      implode hd args) in\r
 246   let sigma = (var, aux 0 false (V var)) :: p.sigma in\r
 247   {p with tms=List.map (aux 0 false) p.tms; sigma}\r
 248 ;;\r
 249 \r
 250 let finish p = assert false ;;\r
 251 \r
 252 let rec auto p = assert false ;;\r
 253 \r
 254 let problem_of (label, div, convs, ps, var_names) =\r
 255  print_hline ();\r
 256  let rec aux = function\r
 257  | `Lam(_,t) -> L (aux t)\r
 258  | `I ((v,_), args) -> Listx.fold_left (fun x y -> mk_app true x (aux y)) (V v) args\r
 259  | `Var(v,_) -> V v\r
 260  | `N _ | `Match _ -> assert false in\r
 261  let convs = (List.rev convs :> Num.nf list) in\r
 262  let tms = List.map aux (convs @ (ps :> Num.nf list)) in\r
 263  let tms = match div with\r
 264  | Some div -> aux (div :> Num.nf) :: tms\r
 265  | None -> tms in\r
 266  let varno = List.length var_names in\r
 267  let p = {orig_freshno=varno; freshno=1+varno; tms; sigma=[]} in\r
 268  (* initial sanity check *)\r
 269  sanity p\r
 270 ;;\r
 271 \r
 272 let rec interactive p =\r
 273  print_string "[varno index alphano] ";\r
 274  let s = read_line () in\r
 275  let spl = Str.split (Str.regexp " +") s in\r
 276  let nth n = int_of_string (List.nth spl n) in\r
 277  let p = step (nth 0) (nth 1) (nth 2) p in\r
 278  interactive (sanity p)\r
 279 ;;\r
 280 \r
 281 let solve p =\r
 282  let rec aux = function\r
 283  | [] -> false\r
 284  | x::xs -> List.exists (eta_subterm x) xs || aux xs in\r
 285  if aux p.tms\r
 286   then print_endline "!!! Problem stopped: subterm problem !!!"\r
 287   else check p (interactive p)\r
 288 ;;\r
 289 \r
 290 Problems.main (solve ++ problem_of);\r